--- 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 *)