renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)

--- a/src/Doc/Datatypes/Datatypes.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -119,7 +119,7 @@
 \item Section
 \ref{sec:deriving-destructors-and-theorems-for-free-constructors},
 ``Deriving Destructors and Theorems for Free Constructors,'' explains how to
-use the command @{command wrap_free_constructors} to derive destructor constants
+use the command @{command free_constructors} to derive destructor constants
 and theorems for freely generated types, as performed internally by @{command
 datatype_new} and @{command codatatype}.
 
@@ -687,7 +687,7 @@
 
 \item The \emph{free constructor theorems} are properties about the constructors
 and destructors that can be derived for any freely generated type. Internally,
-the derivation is performed by @{command wrap_free_constructors}.
+the derivation is performed by @{command free_constructors}.
 
 \item The \emph{functorial theorems} are properties of datatypes related to
 their BNF nature.
@@ -1016,8 +1016,8 @@
 with nested recursion through old-style datatypes, the old-style
 datatypes can be registered as a BNF
 (Section~\ref{sec:introducing-bounded-natural-functors}). If the goal is
-to derive discriminators and selectors, this can be achieved using @{command
-wrap_free_constructors}
+to derive discriminators and selectors, this can be achieved using
+@{command free_constructors}
 (Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
 *}
 
@@ -2588,7 +2588,7 @@
 text {*
 The derivation of convenience theorems for types equipped with free constructors,
 as performed internally by @{command datatype_new} and @{command codatatype},
-is available as a stand-alone command called @{command wrap_free_constructors}.
+is available as a stand-alone command called @{command free_constructors}.
 
 %  * need for this is rare but may arise if you want e.g. to add destructors to
 %    a type not introduced by ...
@@ -2596,7 +2596,7 @@
 %  * also useful for compatibility with old package, e.g. add destructors to
 %    old \keyw{datatype}
 %
-%  * @{command wrap_free_constructors}
+%  * @{command free_constructors}
 %    * @{text "no_discs_sels"}, @{text "no_code"}
 %    * hack to have both co and nonco view via locale (cf. ext nats)
 %  * code generator
@@ -2619,11 +2619,11 @@
 
 text {*
 \begin{matharray}{rcl}
-  @{command_def "wrap_free_constructors"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
+  @{command_def "free_constructors"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
 \end{matharray}
 
 @{rail \<open>
-  @@{command wrap_free_constructors} target? @{syntax dt_options} \<newline>
+  @@{command free_constructors} target? @{syntax dt_options} \<newline>
     term_list name @{syntax wfc_discs_sels}?
   ;
   @{syntax_def wfc_discs_sels}: name_list (name_list_list name_term_list_list? )?

--- a/src/HOL/Ctr_Sugar.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Ctr_Sugar.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -12,7 +12,7 @@
 imports HOL
 keywords
   "print_case_translations" :: diag and
-  "wrap_free_constructors" :: thy_goal
+  "free_constructors" :: thy_goal
 begin
 
 consts

--- a/src/HOL/Nat.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Nat.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -82,7 +82,7 @@
 apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
 done
 
-wrap_free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
+free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
   apply atomize_elim
   apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
  apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
@@ -101,7 +101,7 @@
 
 setup {* Sign.parent_path *}
 
--- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+-- {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
 setup {* Sign.mandatory_path "nat" *}
 
 declare

--- a/src/HOL/Product_Type.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Product_Type.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -12,7 +12,7 @@
 
 subsection {* @{typ bool} is a datatype *}
 
-wrap_free_constructors [True, False] case_bool [=]
+free_constructors [True, False] case_bool [=]
 by auto
 
 text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
@@ -23,7 +23,7 @@
 
 setup {* Sign.parent_path *}
 
-text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
 
 setup {* Sign.mandatory_path "bool" *}
 
@@ -82,7 +82,7 @@
     else SOME (mk_meta_eq @{thm unit_eq})
 *}
 
-wrap_free_constructors ["()"] case_unit
+free_constructors ["()"] case_unit
 by auto
 
 text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
@@ -93,7 +93,7 @@
 
 setup {* Sign.parent_path *}
 
-text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
 
 setup {* Sign.mandatory_path "unit" *}
 
@@ -184,7 +184,7 @@
 lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
   by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
 
-wrap_free_constructors [Pair] case_prod [] [[fst, snd]]
+free_constructors [Pair] case_prod [] [[fst, snd]]
 proof -
   fix P :: bool and p :: "'a \<times> 'b"
   show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
@@ -208,7 +208,7 @@
 
 setup {* Sign.parent_path *}
 
-text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
 
 setup {* Sign.mandatory_path "prod" *}
 

--- a/src/HOL/Sum_Type.thy	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Sum_Type.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -85,7 +85,7 @@
   with assms show P by (auto simp add: sum_def Inl_def Inr_def)
 qed
 
-wrap_free_constructors [Inl, Inr] case_sum [isl] [[projl], [projr]]
+free_constructors [Inl, Inr] case_sum [isl] [[projl], [projr]]
 by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
 
 text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
@@ -102,7 +102,7 @@
 
 setup {* Sign.parent_path *}
 
-text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
 
 setup {* Sign.mandatory_path "sum" *}
 

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
@@ -1250,7 +1250,7 @@
 
             val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
           in
-            wrap_free_constructors tacss (((wrap_opts, ctrs0), standard_binding), (disc_bindings,
+            free_constructors tacss (((wrap_opts, ctrs0), standard_binding), (disc_bindings,
               (sel_bindingss, sel_defaultss))) lthy
           end;
 
@@ -1527,7 +1527,7 @@
   parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
   Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
 
-val parse_co_datatype = parse_wrap_free_constructors_options -- Parse.and_list1 parse_spec;
+val parse_co_datatype = parse_free_constructors_options -- Parse.and_list1 parse_spec;
 
 fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
 

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
@@ -53,11 +53,11 @@
   val dest_case: Proof.context -> string -> typ list -> term ->
     (ctr_sugar * term list * term list) option
 
-  val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
+  val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     (((bool * bool) * term list) * binding) *
       (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
     ctr_sugar * local_theory
-  val parse_wrap_free_constructors_options: (bool * bool) parser
+  val parse_free_constructors_options: (bool * bool) parser
   val parse_bound_term: (binding * string) parser
 end;
 
@@ -278,8 +278,8 @@
 
 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
 
-fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs),
-    raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
+fun prepare_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs), raw_case_binding),
+    (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
 
@@ -946,13 +946,13 @@
     (goalss, after_qed, lthy')
   end;
 
-fun wrap_free_constructors tacss = (fn (goalss, after_qed, lthy) =>
+fun free_constructors tacss = (fn (goalss, after_qed, lthy) =>
   map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
-  |> (fn thms => after_qed thms lthy)) oo prepare_wrap_free_constructors (K I);
+  |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors (K I);
 
-val wrap_free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
+val free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
   Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
-  prepare_wrap_free_constructors Syntax.read_term;
+  prepare_free_constructors Syntax.read_term;
 
 fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
 
@@ -963,7 +963,7 @@
 val parse_bound_terms = parse_bracket_list parse_bound_term;
 val parse_bound_termss = parse_bracket_list parse_bound_terms;
 
-val parse_wrap_free_constructors_options =
+val parse_free_constructors_options =
   Scan.optional (@{keyword "("} |-- Parse.list1
         (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
       @{keyword ")"}
@@ -971,12 +971,12 @@
     (false, false);
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}
-    "wrap an existing freely generated type's constructors"
-    ((parse_wrap_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
+  Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
+    "register an existing freely generated type's constructors"
+    ((parse_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
         @{keyword "]"}) --
       parse_binding -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
         Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
-     >> wrap_free_constructors_cmd);
+     >> free_constructors_cmd);
 
 end;