# HG changeset patch
# User blanchet
# Date 1366907246 -7200
# Node ID 0504e286d66d60911fd7fd24072609ef8a59a6bd
# Parent  67e4ed510dfb747088fe5d5308eba246bd14b76e
renamed "wrap_data" to "wrap_free_constructors"

diff -r 67e4ed510dfb -r 0504e286d66d src/HOL/BNF/BNF_Wrap.thy
--- a/src/HOL/BNF/BNF_Wrap.thy	Thu Apr 25 18:14:04 2013 +0200
+++ b/src/HOL/BNF/BNF_Wrap.thy	Thu Apr 25 18:27:26 2013 +0200
@@ -10,7 +10,7 @@
 theory BNF_Wrap
 imports BNF_Util
 keywords
-  "wrap_data" :: thy_goal and
+  "wrap_free_constructors" :: thy_goal and
   "no_dests" and
   "rep_compat"
 begin
diff -r 67e4ed510dfb -r 0504e286d66d src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 18:14:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 18:27:26 2013 +0200
@@ -534,8 +534,8 @@
 
             val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
           in
-            wrap_datatype tacss (((wrap_opts, ctrs0), casex0), (disc_bindings, (sel_bindingss,
-              sel_defaultss))) lthy
+            wrap_free_constructors tacss (((wrap_opts, ctrs0), casex0), (disc_bindings,
+              (sel_bindingss, sel_defaultss))) lthy
           end;
 
         fun derive_maps_sets_rels (wrap_res, lthy) =
diff -r 67e4ed510dfb -r 0504e286d66d src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 25 18:14:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 25 18:27:26 2013 +0200
@@ -18,7 +18,7 @@
   val name_of_ctr: term -> string
   val name_of_disc: term -> string
 
-  val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
+  val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     (((bool * bool) * term list) * term) *
       (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
     (term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
@@ -123,7 +123,7 @@
 
 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
 
-fun prepare_wrap_datatype prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case),
+fun prepare_wrap_free_constructors prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case),
     (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
@@ -673,13 +673,13 @@
     (goalss, after_qed, lthy')
   end;
 
-fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) =>
+fun wrap_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_datatype (K I);
+  |> (fn thms => after_qed thms lthy)) oo prepare_wrap_free_constructors (K I);
 
-val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
+val wrap_free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
   Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
-  prepare_wrap_datatype Syntax.read_term;
+  prepare_wrap_free_constructors Syntax.read_term;
 
 fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
 
@@ -696,10 +696,11 @@
     >> (pairself (exists I) o split_list)) (false, false);
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wrap an existing datatype"
+  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}
+    "wrap an existing (co)datatype's constructors"
     ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
       Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
         Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
-     >> wrap_datatype_cmd);
+     >> wrap_free_constructors_cmd);
 
 end;