--- 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"];
--- 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 *)
--- 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;
--- 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,
--- 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 *)
--- 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;