# HG changeset patch
# User blanchet
# Date 1428682981 -7200
# Node ID ba8fa0c38d66f7a7ab22a2a9cfa7eeaddd06aa69
# Parent  50cf9e0ae818b2ec5e1f04cd72096afa245b41e2
renamed ML funs

diff -r 50cf9e0ae818 -r ba8fa0c38d66 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 10 14:44:08 2015 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 10 18:23:01 2015 +0200
@@ -190,7 +190,7 @@
         val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
       in
         thy' |>
-        BNF_LFP_Compat.add_primrec_global
+        BNF_LFP_Compat.primrec_global
           [(Binding.name swap_name, SOME swapT, NoSyn)]
           [(Attrib.empty_binding, def1)] ||>
         Sign.parent_path ||>>
@@ -224,7 +224,7 @@
                     Const (swap_name, swapT) $ x $ (prm $ xs $ a)));
       in
         thy' |>
-        BNF_LFP_Compat.add_primrec_global
+        BNF_LFP_Compat.primrec_global
           [(Binding.name prm_name, SOME prmT, NoSyn)]
           [(Attrib.empty_binding, def1), (Attrib.empty_binding, def2)] ||>
         Sign.parent_path
diff -r 50cf9e0ae818 -r ba8fa0c38d66 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Apr 10 14:44:08 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Apr 10 18:23:01 2015 +0200
@@ -256,7 +256,7 @@
       end) descr;
 
     val (perm_simps, thy2) =
-      BNF_LFP_Compat.add_primrec_overloaded
+      BNF_LFP_Compat.primrec_overloaded
         (map (fn (s, sT) => (s, sT, false))
            (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
         (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1;
diff -r 50cf9e0ae818 -r ba8fa0c38d66 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Apr 10 14:44:08 2015 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Apr 10 18:23:01 2015 +0200
@@ -8,11 +8,11 @@
 
 signature NOMINAL_PRIMREC =
 sig
-  val add_primrec: term list option -> term option ->
+  val primrec: term list option -> term option ->
     (binding * typ option * mixfix) list ->
     (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> local_theory -> Proof.state
-  val add_primrec_cmd: string list option -> string option ->
+  val primrec_cmd: string list option -> string option ->
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> local_theory -> Proof.state
@@ -382,8 +382,8 @@
 
 in
 
-val add_primrec = gen_primrec Specification.check_spec (K I);
-val add_primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term;
+val primrec = gen_primrec Specification.check_spec (K I);
+val primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term;
 
 end;
 
@@ -407,7 +407,7 @@
     "define primitive recursive functions on nominal datatypes"
     (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
       >> (fn ((((invs, fctxt), fixes), params), specs) =>
-        add_primrec_cmd invs fctxt fixes params specs));
+        primrec_cmd invs fctxt fixes params specs));
 
 end;
 
diff -r 50cf9e0ae818 -r ba8fa0c38d66 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Apr 10 14:44:08 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Apr 10 18:23:01 2015 +0200
@@ -70,10 +70,10 @@
   val gfp_rec_sugar_interpretation: string ->
     (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
 
-  val add_primcorecursive_cmd: corec_option list ->
+  val primcorecursive_cmd: corec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
     Proof.context -> Proof.state
-  val add_primcorec_cmd: corec_option list ->
+  val primcorec_cmd: corec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
     local_theory -> local_theory
 end;
@@ -1041,7 +1041,7 @@
 fun is_trivial_implies thm =
   uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm));
 
-fun add_primcorec_ursive auto opts fixes specs of_specs_opt lthy =
+fun primcorec_ursive auto opts fixes specs of_specs_opt lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
@@ -1527,7 +1527,7 @@
     (goalss, after_qed, lthy')
   end;
 
-fun add_primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy =
+fun primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy =
   let
     val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes);
     val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups));
@@ -1536,18 +1536,18 @@
       split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
     val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
   in
-    add_primcorec_ursive auto opts fixes specs of_specs_opt lthy
+    primcorec_ursive auto opts fixes specs of_specs_opt lthy
   end;
 
-val add_primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
+val primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
   lthy
   |> Proof.theorem NONE after_qed goalss
   |> Proof.refine (Method.primitive_text (K I))
-  |> Seq.hd) ooo add_primcorec_ursive_cmd false;
+  |> Seq.hd) ooo primcorec_ursive_cmd false;
 
-val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
+val primcorec_cmd = (fn (goalss, after_qed, lthy) =>
     lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo
-  add_primcorec_ursive_cmd true;
+  primcorec_ursive_cmd true;
 
 val corec_option_parser = Parse.group (K "option")
   (Plugin_Name.parse_filter >> Plugins_Option
@@ -1562,13 +1562,13 @@
   "define primitive corecursive functions"
   ((Scan.optional (@{keyword "("} |--
       Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
-    (Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorecursive_cmd);
+    (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorecursive_cmd);
 
 val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
   "define primitive corecursive functions"
   ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
       --| @{keyword ")"}) []) --
-    (Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorec_cmd);
+    (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorec_cmd);
 
 val _ = Theory.setup (gfp_rec_sugar_interpretation Transfer_BNF.transfer_plugin
   gfp_rec_sugar_transfer_interpretation);
diff -r 50cf9e0ae818 -r ba8fa0c38d66 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Apr 10 14:44:08 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Apr 10 18:23:01 2015 +0200
@@ -26,14 +26,14 @@
   val datatype_compat_global: string list -> theory -> theory
   val datatype_compat_cmd: string list -> local_theory -> local_theory
   val add_datatype: preference list -> Old_Datatype_Aux.spec list -> theory -> string list * theory
-  val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
+  val primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
     local_theory -> (term list * thm list) * local_theory
-  val add_primrec_global: (binding * typ option * mixfix) list ->
+  val primrec_global: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
-  val add_primrec_overloaded: (string * (string * typ) * bool) list ->
+  val primrec_overloaded: (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory ->
     (term list * thm list) * theory
-  val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
+  val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
     local_theory -> (string list * (term list * thm list)) * local_theory
 end;
 
@@ -532,11 +532,10 @@
      |> not (member (op =) prefs Keep_Nesting) ? perhaps (try (datatype_compat_global fpT_names)))
   end;
 
-val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
-val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global;
-val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded;
-val add_primrec_simple = apfst (apsnd (apsnd (flat o snd))) ooo
-  BNF_LFP_Rec_Sugar.add_primrec_simple;
+val primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.primrec;
+val primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.primrec_global;
+val primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded;
+val primrec_simple = apfst (apsnd (apsnd (flat o snd))) ooo BNF_LFP_Rec_Sugar.primrec_simple;
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword datatype_compat}
diff -r 50cf9e0ae818 -r ba8fa0c38d66 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Apr 10 14:44:08 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Apr 10 18:23:01 2015 +0200
@@ -61,16 +61,16 @@
   val lfp_rec_sugar_interpretation: string ->
     (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
 
-  val add_primrec: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> local_theory -> (term list * thm list list) * local_theory
-  val add_primrec_cmd: rec_option list -> (binding * string option * mixfix) list ->
+  val primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
+    local_theory -> (term list * thm list list) * local_theory
+  val primrec_cmd: rec_option list -> (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> local_theory -> (term list * thm list list) * local_theory
-  val add_primrec_global: (binding * typ option * mixfix) list ->
+  val primrec_global: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> (term list * thm list list) * theory
-  val add_primrec_overloaded: (string * (string * typ) * bool) list ->
+  val primrec_overloaded: (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> (term list * thm list list) * theory
-  val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
+  val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
     local_theory -> (string list * (term list * (int list list * thm list list))) * local_theory
 end;
 
@@ -591,7 +591,7 @@
       lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
   end;
 
-fun add_primrec_simple0 plugins nonexhaustive transfer fixes ts lthy =
+fun primrec_simple0 plugins nonexhaustive transfer fixes ts lthy =
   let
     val actual_nn = length fixes;
 
@@ -608,10 +608,10 @@
       in ((names, (map fst defs, thms)), lthy) end)
   end;
 
-fun add_primrec_simple fixes ts lthy =
-  add_primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy
+fun primrec_simple fixes ts lthy =
+  primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy
   handle OLD_PRIMREC () =>
-    Old_Primrec.add_primrec_simple fixes ts lthy
+    Old_Primrec.primrec_simple fixes ts lthy
     |>> apsnd (apsnd (pair [] o single)) o apfst single;
 
 fun gen_primrec old_primrec prep_spec opts
@@ -643,7 +643,7 @@
         end);
   in
     lthy
-    |> add_primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs)
+    |> primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs)
     |-> (fn (names, (ts, (jss, simpss))) =>
       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
       #> Local_Theory.notes (mk_notes jss names simpss)
@@ -651,17 +651,17 @@
   end
   handle OLD_PRIMREC () => old_primrec raw_fixes raw_specs lthy |>> apsnd single;
 
-val add_primrec = gen_primrec Old_Primrec.add_primrec Specification.check_spec [];
-val add_primrec_cmd = gen_primrec Old_Primrec.add_primrec_cmd Specification.read_spec;
+val primrec = gen_primrec Old_Primrec.primrec Specification.check_spec [];
+val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_spec;
 
-fun add_primrec_global fixes specs =
+fun primrec_global fixes specs =
   Named_Target.theory_init
-  #> add_primrec fixes specs
+  #> primrec fixes specs
   ##> Local_Theory.exit_global;
 
-fun add_primrec_overloaded ops fixes specs =
+fun primrec_overloaded ops fixes specs =
   Overloading.overloading ops
-  #> add_primrec fixes specs
+  #> primrec fixes specs
   ##> Local_Theory.exit_global;
 
 val rec_option_parser = Parse.group (K "option")
@@ -674,6 +674,6 @@
   ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
       --| @{keyword ")"}) []) --
     (Parse.fixes -- Parse_Spec.where_alt_specs)
-    >> (fn (opts, (fixes, specs)) => snd o add_primrec_cmd opts fixes specs));
+    >> (fn (opts, (fixes, specs)) => snd o primrec_cmd opts fixes specs));
 
 end;
diff -r 50cf9e0ae818 -r ba8fa0c38d66 src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Fri Apr 10 14:44:08 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Fri Apr 10 18:23:01 2015 +0200
@@ -8,16 +8,16 @@
 
 signature OLD_PRIMREC =
 sig
-  val add_primrec: (binding * typ option * mixfix) list ->
+  val primrec: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> local_theory -> (term list * thm list) * local_theory
-  val add_primrec_cmd: (binding * string option * mixfix) list ->
+  val primrec_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> local_theory -> (term list * thm list) * local_theory
-  val add_primrec_global: (binding * typ option * mixfix) list ->
+  val primrec_global: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
-  val add_primrec_overloaded: (string * (string * typ) * bool) list ->
+  val primrec_overloaded: (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
-  val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
+  val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
     local_theory -> (string * (term list * thm list)) * local_theory
 end;
 
@@ -260,7 +260,7 @@
 
 (* primrec definition *)
 
-fun add_primrec_simple fixes ts lthy =
+fun primrec_simple fixes ts lthy =
   let
     val ((prefix, (_, defs)), prove) = distill lthy fixes ts;
   in
@@ -280,7 +280,7 @@
       (Binding.qualify true prefix (Binding.name "simps"), @{attributes [simp, nitpick_simp]});
   in
     lthy
-    |> add_primrec_simple fixes (map snd spec)
+    |> primrec_simple fixes (map snd spec)
     |-> (fn (prefix, (ts, simps)) =>
       Spec_Rules.add Spec_Rules.Equational (ts, simps)
       #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
@@ -290,22 +290,22 @@
 
 in
 
-val add_primrec = gen_primrec Specification.check_spec;
-val add_primrec_cmd = gen_primrec Specification.read_spec;
+val primrec = gen_primrec Specification.check_spec;
+val primrec_cmd = gen_primrec Specification.read_spec;
 
 end;
 
-fun add_primrec_global fixes specs thy =
+fun primrec_global fixes specs thy =
   let
     val lthy = Named_Target.theory_init thy;
-    val ((ts, simps), lthy') = add_primrec fixes specs lthy;
+    val ((ts, simps), lthy') = primrec fixes specs lthy;
     val simps' = Proof_Context.export lthy' lthy simps;
   in ((ts, simps'), Local_Theory.exit_global lthy') end;
 
-fun add_primrec_overloaded ops fixes specs thy =
+fun primrec_overloaded ops fixes specs thy =
   let
     val lthy = Overloading.overloading ops thy;
-    val ((ts, simps), lthy') = add_primrec fixes specs lthy;
+    val ((ts, simps), lthy') = primrec fixes specs lthy;
     val simps' = Proof_Context.export lthy' lthy simps;
   in ((ts, simps'), Local_Theory.exit_global lthy') end;
 
diff -r 50cf9e0ae818 -r ba8fa0c38d66 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Apr 10 14:44:08 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Apr 10 18:23:01 2015 +0200
@@ -96,7 +96,7 @@
       subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
     val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
     val ((_, (_, eqs2)), lthy') = lthy
-      |> BNF_LFP_Compat.add_primrec_simple
+      |> BNF_LFP_Compat.primrec_simple
         [((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1;
     val cT_random_aux = inst pt_random_aux;
     val cT_rhs = inst pt_rhs;
diff -r 50cf9e0ae818 -r ba8fa0c38d66 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Fri Apr 10 14:44:08 2015 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Fri Apr 10 18:23:01 2015 +0200
@@ -8,8 +8,8 @@
 
 signature PRIMREC_PACKAGE =
 sig
-  val add_primrec: ((binding * string) * Token.src list) list -> theory -> theory * thm list
-  val add_primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
+  val primrec: ((binding * string) * Token.src list) list -> theory -> theory * thm list
+  val primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
 end;
 
 structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -161,7 +161,7 @@
 
 (* prepare functions needed for definitions *)
 
-fun add_primrec_i args thy =
+fun primrec_i args thy =
   let
     val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args);
     val SOME (fname, ftype, ls, rs, con_info, eqns) =
@@ -188,8 +188,8 @@
       ||> Sign.parent_path;
   in (thy3, eqn_thms') end;
 
-fun add_primrec args thy =
-  add_primrec_i (map (fn ((name, s), srcs) =>
+fun primrec args thy =
+  primrec_i (map (fn ((name, s), srcs) =>
     ((name, Syntax.read_prop_global thy s), map (Attrib.attribute_cmd_global thy) srcs))
     args) thy;
 
@@ -199,7 +199,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword primrec} "define primitive recursive functions on datatypes"
     (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
-      >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
+      >> (Toplevel.theory o (#1 oo (primrec o map Parse.triple_swap))));
 
 end;