--- a/src/HOL/Library/BNF_Axiomatization.thy Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/Library/BNF_Axiomatization.thy Tue Mar 24 18:10:56 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
--- a/src/HOL/Tools/BNF/bnf_comp.ML Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Tue Mar 24 18:10:56 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);
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Mar 24 18:10:56 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 [])
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 24 18:10:56 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
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Mar 24 18:10:56 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);
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 24 18:10:56 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;