# HG changeset patch
# User wenzelm
# Date 1427236782 -3600
# Node ID db0b87085c168d028a394c5fc011d4c3f4a678de
# Parent  39442248a027a418fbf73a8b95e470462027eb07# Parent  88a89f01fc27952499f2fe8dea0e515860e50075
merged

diff -r 88a89f01fc27 -r db0b87085c16 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Mar 24 23:37:05 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Mar 24 23:39:42 2015 +0100
@@ -969,12 +969,12 @@
 \item[@{text "t."}\hthm{map_cong_simp}\rm:] ~ \\
 @{thm list.map_cong_simp[no_vars]}
 
+\item[@{text "t."}\hthm{map_id0}\rm:] ~ \\
+@{thm list.map_id0[no_vars]}
+
 \item[@{text "t."}\hthm{map_id}\rm:] ~ \\
 @{thm list.map_id[no_vars]}
 
-\item[@{text "t."}\hthm{map_id0}\rm:] ~ \\
-@{thm list.map_id0[no_vars]}
-
 \item[@{text "t."}\hthm{map_ident}\rm:] ~ \\
 @{thm list.map_ident[no_vars]}
 
@@ -1001,14 +1001,14 @@
 @{thm list.rel_map(1)[no_vars]} \\
 @{thm list.rel_map(2)[no_vars]}
 
-\item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\
-@{thm list.rel_refl[no_vars]}
-
 \item[@{text "t."}\hthm{rel_mono} @{text "[mono, relator_mono]"}\rm:] ~ \\
 @{thm list.rel_mono[no_vars]} \\
 The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin
 (Section~\ref{ssec:lifting}).
 
+\item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\
+@{thm list.rel_refl[no_vars]}
+
 \item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.rel_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
diff -r 88a89f01fc27 -r db0b87085c16 src/HOL/Library/BNF_Axiomatization.thy
--- a/src/HOL/Library/BNF_Axiomatization.thy	Tue Mar 24 23:37:05 2015 +0100
+++ b/src/HOL/Library/BNF_Axiomatization.thy	Tue Mar 24 23:39:42 2015 +0100
@@ -5,7 +5,7 @@
 Axiomatic declaration of bounded natural functors.
 *)
 
-section {* Axiomatic declaration of Bounded Natural Functors *}
+section {* Axiomatic Declaration of Bounded Natural Functors *}
 
 theory BNF_Axiomatization
 imports Main
diff -r 88a89f01fc27 -r db0b87085c16 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Tue Mar 24 23:37:05 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -8,7 +8,7 @@
 
 signature BNF_COMP =
 sig
-  val bnf_inline_threshold: int Config.T
+  val inline_threshold: int Config.T
 
   val ID_bnf: BNF_Def.bnf
   val DEADID_bnf: BNF_Def.bnf
@@ -76,7 +76,7 @@
 open BNF_Tactics
 open BNF_Comp_Tactics
 
-val bnf_inline_threshold = Attrib.setup_config_int @{binding bnf_inline_threshold} (K 5);
+val inline_threshold = Attrib.setup_config_int @{binding bnf_inline_threshold} (K 5);
 
 val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
 val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
@@ -756,7 +756,7 @@
 
 fun maybe_typedef ctxt force_out_of_line (b, As, mx) set opt_morphs tac =
   let
-    val threshold = Config.get ctxt bnf_inline_threshold;
+    val threshold = Config.get ctxt inline_threshold;
     val repT = HOLogic.dest_setT (fastype_of set);
     val out_of_line = force_out_of_line orelse
       (threshold >= 0 andalso Term.size_of_typ repT > threshold);
diff -r 88a89f01fc27 -r db0b87085c16 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 24 23:37:05 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -2367,7 +2367,7 @@
         |> Local_Theory.notes (common_notes @ notes)
         (* for "datatype_realizer.ML": *)
         |>> name_noted_thms
-          (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN
+          (fst (dest_Type (hd fpTs)) ^ implode (map (prefix "_") (tl fp_b_names))) inductN
         |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
           fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs
           map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
diff -r 88a89f01fc27 -r db0b87085c16 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Mar 24 23:37:05 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -106,9 +106,7 @@
 val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs;
 
 fun mk_case_transfer_tac ctxt rel_cases cases =
-  let
-    val n = length (tl (Thm.prems_of rel_cases));
-  in
+  let val n = length (tl (Thm.prems_of rel_cases)) in
     REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
     HEADGOAL (etac rel_cases) THEN
     ALLGOALS (hyp_subst_tac ctxt) THEN
diff -r 88a89f01fc27 -r db0b87085c16 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 24 23:37:05 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -112,7 +112,8 @@
 fun unexpected_corec_call ctxt eqns t =
   error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
 fun use_primcorecursive () =
-  error "\"auto\" failed (try \"primcorecursive\" instead of \"primcorec\")";
+  error ("\"auto\" failed (try " ^ quote (#1 @{command_spec "primcorecursive"}) ^ " instead of " ^
+    quote (#1 @{command_spec "primcorec"}) ^ ")");
 
 datatype corec_option =
   Plugins_Option of Proof.context -> Plugin_Name.filter |
@@ -1552,21 +1553,20 @@
    || Parse.reserved "exhaustive" >> K Exhaustive_Option
    || Parse.reserved "transfer" >> K Transfer_Option);
 
-(* FIXME: should use "Parse_Spec.spec" instead of "Parse.prop" and honor binding *)
-val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
+val where_alt_props_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
   ((Parse.prop >> pair Attrib.empty_binding) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
 
 val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
   "define primitive corecursive functions"
   ((Scan.optional (@{keyword "("} |--
       Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
-    (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorecursive_cmd);
+    (Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorecursive_cmd);
 
 val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
   "define primitive corecursive functions"
   ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
       --| @{keyword ")"}) []) --
-    (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd);
+    (Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorec_cmd);
 
 val _ = Theory.setup (gfp_rec_sugar_interpretation Transfer_BNF.transfer_plugin
   gfp_rec_sugar_transfer_interpretation);
diff -r 88a89f01fc27 -r db0b87085c16 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 24 23:37:05 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 24 23:39:42 2015 +0100
@@ -329,9 +329,9 @@
       end;
 
     val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
-        lthy
-        |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
-        ||> `Local_Theory.restore;
+      lthy
+      |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
+      ||> `Local_Theory.restore;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
@@ -652,11 +652,11 @@
       end;
 
     val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
-        lthy
-        |> fold_map (fn i => Local_Theory.define
-          ((min_alg_bind i, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks
-        |>> apsnd split_list o split_list
-        ||> `Local_Theory.restore;
+      lthy
+      |> fold_map (fn i => Local_Theory.define
+        ((min_alg_bind i, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks
+      |>> apsnd split_list o split_list
+      ||> `Local_Theory.restore;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;