Rename split command to make_binder_inductive

jvanbruegge · Oct 15, 2024 · e94facf · e94facf
1 parent 3328d50
commit e94facf
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/Tools/binder_inductive.ML b/Tools/binder_inductive.ML
@@ -1014,7 +1014,7 @@ val binder_inductive_parser = Parse.name -- Scan.option (
   ) -- parse_perm_supps
 
 val _ =
-  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>binder_inductive_split\<close> "derive strengthened induction theorems for inductive predicates"
+  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>make_binder_inductive\<close> "derive strengthened induction theorems for inductive predicates"
     (binder_inductive_parser >> binder_inductive_cmd);
 
 end
diff --git a/thys/MRBNF_Recursor.thy b/thys/MRBNF_Recursor.thy
@@ -2,7 +2,7 @@ theory MRBNF_Recursor
   imports MRBNF_FP
   keywords "binder_datatype" :: thy_defn
     and "binder_inductive" :: thy_goal_defn
-    and "binder_inductive_split" :: thy_goal_defn
+    and "make_binder_inductive" :: thy_goal_defn
     and "binds"
 begin
 

diff --git a/thys/POPLmark/SystemFSub.thy b/thys/POPLmark/SystemFSub.thy
@@ -281,7 +281,7 @@ declare ty.intros[intro]
 lemma ty_fresh_extend: "\<Gamma>, x <: U \<turnstile> S <: T \<Longrightarrow> x \<notin> dom \<Gamma> \<union> FFVars_ctxt \<Gamma> \<and> x \<notin> FFVars_typ U"
   by (metis (no_types, lifting) UnE fst_conv snd_conv subsetD wf_ConsE wf_FFVars wf_context)
 
-binder_inductive_split ty
+make_binder_inductive ty
   subgoal for R B \<sigma> \<Gamma> T1 T2
     unfolding split_beta
     by (elim disj_forward exE)