# HG changeset patch # User wenzelm # Date 1206792185 -3600 # Node ID 3cc1e48d0ce19b638d01c3ecc42d2b161a72627c # Parent 94735cff132c8066b5af9621795b5a6df8773144 eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!); diff -r 94735cff132c -r 3cc1e48d0ce1 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Fri Mar 28 22:39:47 2008 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Sat Mar 29 13:03:05 2008 +0100 @@ -559,13 +559,12 @@ val rep_set_names'' = map (Sign.full_name thy3) rep_set_names'; val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) = - setmp InductivePackage.quiet_mode false - (InductivePackage.add_inductive_global (serial_string ()) - {verbose = false, kind = Thm.internalK, + InductivePackage.add_inductive_global (serial_string ()) + {quiet_mode = false, verbose = false, kind = Thm.internalK, alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false} (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn)) (rep_set_names' ~~ recTs')) - [] (map (fn x => (("", []), x)) intr_ts) []) thy3; + [] (map (fn x => (("", []), x)) intr_ts) [] thy3; (**** Prove that representing set is closed under permutation ****) @@ -609,13 +608,12 @@ val (typedefs, thy6) = thy5 |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy => - setmp TypedefPackage.quiet_mode true - (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) + TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ Const (cname, U --> HOLogic.boolT)) NONE (rtac exI 1 THEN rtac CollectI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) - (resolve_tac rep_intrs 1))) thy |> (fn ((_, r), thy) => + (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) => let val permT = mk_permT (TFree (Name.variant tvs "'a", HOLogic.typeS)); val pi = Free ("pi", permT); @@ -1484,13 +1482,12 @@ val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) = thy10 |> - setmp InductivePackage.quiet_mode (!quiet_mode) - (InductivePackage.add_inductive_global (serial_string ()) - {verbose = false, kind = Thm.internalK, + InductivePackage.add_inductive_global (serial_string ()) + {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false} (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) - (map (fn x => (("", []), x)) rec_intr_ts) []) ||> + (map (fn x => (("", []), x)) rec_intr_ts) [] ||> PureThy.hide_thms true [NameSpace.append (Sign.full_name thy10 big_rec_name) "induct"]; diff -r 94735cff132c -r 3cc1e48d0ce1 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Mar 28 22:39:47 2008 +0100 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Sat Mar 29 13:03:05 2008 +0100 @@ -154,13 +154,12 @@ (([], 0), descr' ~~ recTs ~~ rec_sets'); val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) = - setmp InductivePackage.quiet_mode (!quiet_mode) - (InductivePackage.add_inductive_global (serial_string ()) - {verbose = false, kind = Thm.internalK, alt_name = big_rec_name', - coind = false, no_elim = false, no_ind = true} + InductivePackage.add_inductive_global (serial_string ()) + {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, + alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true} (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) - (map (fn x => (("", []), x)) rec_intr_ts) []) thy0; + (map (fn x => (("", []), x)) rec_intr_ts) [] thy0; (* prove uniqueness and termination of primrec combinators *) diff -r 94735cff132c -r 3cc1e48d0ce1 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Mar 28 22:39:47 2008 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Sat Mar 29 13:03:05 2008 +0100 @@ -176,24 +176,22 @@ ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names')); val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) = - setmp InductivePackage.quiet_mode (! quiet_mode) - (InductivePackage.add_inductive_global (serial_string ()) - {verbose = false, kind = Thm.internalK, alt_name = big_rec_name, + InductivePackage.add_inductive_global (serial_string ()) + {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false} (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') [] - (map (fn x => (("", []), x)) intr_ts) []) thy1; + (map (fn x => (("", []), x)) intr_ts) [] thy1; (********************************* typedef ********************************) val (typedefs, thy3) = thy2 |> parent_path flat_names |> fold_map (fn ((((name, mx), tvs), c), name') => - setmp TypedefPackage.quiet_mode true - (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) + TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) (Collect $ Const (c, UnivT')) NONE (rtac exI 1 THEN rtac CollectI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) - (resolve_tac rep_intrs 1)))) + (resolve_tac rep_intrs 1))) (types_syntax ~~ tyvars ~~ (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||> add_path flat_names big_name; diff -r 94735cff132c -r 3cc1e48d0ce1 src/HOL/Tools/function_package/inductive_wrap.ML --- a/src/HOL/Tools/function_package/inductive_wrap.ML Fri Mar 28 22:39:47 2008 +0100 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML Sat Mar 29 13:03:05 2008 +0100 @@ -41,7 +41,8 @@ let val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) = InductivePackage.add_inductive_i - {verbose = ! Toplevel.debug, + {quiet_mode = false, + verbose = ! Toplevel.debug, kind = Thm.internalK, alt_name = "", coind = false, diff -r 94735cff132c -r 3cc1e48d0ce1 src/HOL/Tools/inductive_set_package.ML --- a/src/HOL/Tools/inductive_set_package.ML Fri Mar 28 22:39:47 2008 +0100 +++ b/src/HOL/Tools/inductive_set_package.ML Sat Mar 29 13:03:05 2008 +0100 @@ -12,7 +12,8 @@ val to_pred_att: thm list -> attribute val pred_set_conv_att: attribute val add_inductive_i: - {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} -> + {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring, + coind: bool, no_elim: bool, no_ind: bool} -> ((string * typ) * mixfix) list -> (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list -> local_theory -> InductivePackage.inductive_result * local_theory @@ -401,7 +402,7 @@ (**** definition of inductive sets ****) -fun add_ind_set_def {verbose, kind, alt_name, coind, no_elim, no_ind} +fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind} cs intros monos params cnames_syn ctxt = let val thy = ProofContext.theory_of ctxt; @@ -464,8 +465,8 @@ val cnames_syn' = map (fn (s, _) => (s ^ "p", NoSyn)) cnames_syn; val monos' = map (to_pred [] (Context.Proof ctxt)) monos; val ({preds, intrs, elims, raw_induct, ...}, ctxt1) = - InductivePackage.add_ind_def {verbose = verbose, kind = kind, alt_name = "", - coind = coind, no_elim = no_elim, no_ind = no_ind} + InductivePackage.add_ind_def {quiet_mode = quiet_mode, verbose = verbose, kind = kind, + alt_name = "", coind = coind, no_elim = no_elim, no_ind = no_ind} cs' intros' monos' params1 cnames_syn' ctxt; (* define inductive sets using previously defined predicates *) diff -r 94735cff132c -r 3cc1e48d0ce1 src/HOL/Tools/typecopy_package.ML --- a/src/HOL/Tools/typecopy_package.ML Fri Mar 28 22:39:47 2008 +0100 +++ b/src/HOL/Tools/typecopy_package.ML Sat Mar 29 13:03:05 2008 +0100 @@ -106,9 +106,8 @@ end in thy - |> setmp TypedefPackage.quiet_mode true - (TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn) - (HOLogic.mk_UNIV ty) (Option.map swap constr_proj)) tac + |> TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn) + (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac |-> (fn (tyco, info) => add_info tyco info) end;