tuning

--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Aug 01 14:22:10 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Aug 01 14:22:21 2013 +0200
@@ -42,7 +42,7 @@
     (((bool * bool) * term list) * term) *
       (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
     ctr_sugar * local_theory
-  val parse_wrap_options: (bool * bool) parser
+  val parse_wrap_free_constructors_options: (bool * bool) parser
   val parse_bound_term: (binding * string) parser
 end;
 
@@ -753,7 +753,7 @@
 val parse_bound_terms = parse_bracket_list parse_bound_term;
 val parse_bound_termss = parse_bracket_list parse_bound_terms;
 
-val parse_wrap_options =
+val parse_wrap_free_constructors_options =
   Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_dests"} >> K (true, false)) ||
       (@{keyword "rep_compat"} >> K (false, true))) --| @{keyword ")"}
     >> (pairself (exists I) o split_list)) (false, false);
@@ -761,7 +761,8 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}
     "wrap an existing freely generated type's constructors"
-    ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
+    ((parse_wrap_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
+        @{keyword "]"}) --
       Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
         Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
      >> wrap_free_constructors_cmd);

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 01 14:22:10 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 01 14:22:21 2013 +0200
@@ -1464,7 +1464,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_options -- Parse.and_list1 parse_spec;
+val parse_co_datatype = parse_wrap_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;