1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Mar 29 13:03:07 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Mar 29 13:03:08 2008 +0100
     1.3 @@ -21,7 +21,6 @@
     1.4  
     1.5  signature BASIC_INDUCTIVE_PACKAGE =
     1.6  sig
     1.7 -  val quiet_mode: bool ref
     1.8    type inductive_result
     1.9    val morph_result: morphism -> inductive_result -> inductive_result
    1.10    type inductive_info
    1.11 @@ -39,7 +38,8 @@
    1.12    val inductive_cases_i: ((bstring * Attrib.src list) * term list) list ->
    1.13      Proof.context -> thm list list * local_theory
    1.14    val add_inductive_i:
    1.15 -    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    1.16 +    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
    1.17 +      coind: bool, no_elim: bool, no_ind: bool} ->
    1.18      ((string * typ) * mixfix) list ->
    1.19      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    1.20        local_theory -> inductive_result * local_theory
    1.21 @@ -48,7 +48,8 @@
    1.22      ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
    1.23      local_theory -> inductive_result * local_theory
    1.24    val add_inductive_global: string ->
    1.25 -    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    1.26 +    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
    1.27 +      coind: bool, no_elim: bool, no_ind: bool} ->
    1.28      ((string * typ) * mixfix) list -> (string * typ) list ->
    1.29      ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
    1.30    val arities_of: thm -> (string * int) list
    1.31 @@ -69,7 +70,8 @@
    1.32      thm -> local_theory -> thm list * thm list * thm * local_theory
    1.33    val add_ind_def: add_ind_def
    1.34    val gen_add_inductive_i: add_ind_def ->
    1.35 -    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    1.36 +    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
    1.37 +      coind: bool, no_elim: bool, no_ind: bool} ->
    1.38      ((string * typ) * mixfix) list ->
    1.39      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    1.40        local_theory -> inductive_result * local_theory
    1.41 @@ -192,9 +194,8 @@
    1.42  
    1.43  (** misc utilities **)
    1.44  
    1.45 -val quiet_mode = ref false;
    1.46 -fun message s = if ! quiet_mode then () else writeln s;
    1.47 -fun clean_message s = if ! quick_and_dirty then () else message s;
    1.48 +fun message quiet_mode s = if quiet_mode then () else writeln s;
    1.49 +fun clean_message quiet_mode s = if ! quick_and_dirty then () else message quiet_mode s;
    1.50  
    1.51  fun coind_prefix true = "co"
    1.52    | coind_prefix false = "";
    1.53 @@ -316,8 +317,8 @@
    1.54  
    1.55  (* prove monotonicity -- NOT subject to quick_and_dirty! *)
    1.56  
    1.57 -fun prove_mono predT fp_fun monos ctxt =
    1.58 - (message "  Proving monotonicity ...";
    1.59 +fun prove_mono quiet_mode predT fp_fun monos ctxt =
    1.60 + (message quiet_mode "  Proving monotonicity ...";
    1.61    Goal.prove ctxt [] []   (*NO quick_and_dirty here!*)
    1.62      (HOLogic.mk_Trueprop
    1.63        (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
    1.64 @@ -331,9 +332,9 @@
    1.65  
    1.66  (* prove introduction rules *)
    1.67  
    1.68 -fun prove_intrs coind mono fp_def k params intr_ts rec_preds_defs ctxt =
    1.69 +fun prove_intrs quiet_mode coind mono fp_def k params intr_ts rec_preds_defs ctxt =
    1.70    let
    1.71 -    val _ = clean_message "  Proving the introduction rules ...";
    1.72 +    val _ = clean_message quiet_mode "  Proving the introduction rules ...";
    1.73  
    1.74      val unfold = funpow k (fn th => th RS fun_cong)
    1.75        (mono RS (fp_def RS
    1.76 @@ -359,9 +360,9 @@
    1.77  
    1.78  (* prove elimination rules *)
    1.79  
    1.80 -fun prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt =
    1.81 +fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt =
    1.82    let
    1.83 -    val _ = clean_message "  Proving the elimination rules ...";
    1.84 +    val _ = clean_message quiet_mode "  Proving the elimination rules ...";
    1.85  
    1.86      val ([pname], ctxt') = ctxt |>
    1.87        Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
    1.88 @@ -476,10 +477,10 @@
    1.89  
    1.90  (* prove induction rule *)
    1.91  
    1.92 -fun prove_indrule cs argTs bs xs rec_const params intr_ts mono
    1.93 +fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
    1.94      fp_def rec_preds_defs ctxt =
    1.95    let
    1.96 -    val _ = clean_message "  Proving the induction rule ...";
    1.97 +    val _ = clean_message quiet_mode "  Proving the induction rule ...";
    1.98      val thy = ProofContext.theory_of ctxt;
    1.99  
   1.100      (* predicates for induction rule *)
   1.101 @@ -585,7 +586,7 @@
   1.102  
   1.103  (** specification of (co)inductive predicates **)
   1.104  
   1.105 -fun mk_ind_def alt_name coind cs intr_ts monos params cnames_syn ctxt =
   1.106 +fun mk_ind_def quiet_mode alt_name coind cs intr_ts monos params cnames_syn ctxt =
   1.107    let
   1.108      val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
   1.109  
   1.110 @@ -663,7 +664,7 @@
   1.111      val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
   1.112      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
   1.113  
   1.114 -    val mono = prove_mono predT fp_fun monos ctxt''
   1.115 +    val mono = prove_mono quiet_mode predT fp_fun monos ctxt''
   1.116  
   1.117    in (ctxt'', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
   1.118      list_comb (rec_const, params), preds, argTs, bs, xs)
   1.119 @@ -715,30 +716,31 @@
   1.120    in (intrs', elims', induct', ctxt3) end;
   1.121  
   1.122  type add_ind_def =
   1.123 -  {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
   1.124 +  {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
   1.125 +    coind: bool, no_elim: bool, no_ind: bool} ->
   1.126    term list -> ((string * Attrib.src list) * term) list -> thm list ->
   1.127    term list -> (string * mixfix) list ->
   1.128    local_theory -> inductive_result * local_theory
   1.129  
   1.130 -fun add_ind_def {verbose, kind, alt_name, coind, no_elim, no_ind}
   1.131 +fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind}
   1.132      cs intros monos params cnames_syn ctxt =
   1.133    let
   1.134      val _ = null cnames_syn andalso error "No inductive predicates given";
   1.135 -    val _ =
   1.136 -      if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^
   1.137 -        commas_quote (map fst cnames_syn)) else ();
   1.138 +    val _ = message (quiet_mode andalso not verbose)
   1.139 +      ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^
   1.140 +        commas_quote (map fst cnames_syn));
   1.141  
   1.142      val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn;  (* FIXME *)
   1.143      val ((intr_names, intr_atts), intr_ts) =
   1.144        apfst split_list (split_list (map (check_rule ctxt cs params) intros));
   1.145  
   1.146      val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
   1.147 -      argTs, bs, xs) = mk_ind_def alt_name coind cs intr_ts monos params cnames_syn ctxt;
   1.148 +      argTs, bs, xs) = mk_ind_def quiet_mode alt_name coind cs intr_ts monos params cnames_syn ctxt;
   1.149  
   1.150 -    val (intrs, unfold) = prove_intrs coind mono fp_def (length bs + length xs)
   1.151 +    val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
   1.152        params intr_ts rec_preds_defs ctxt1;
   1.153      val elims = if no_elim then [] else
   1.154 -      prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt1;
   1.155 +      prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt1;
   1.156      val raw_induct = zero_var_indexes
   1.157        (if no_ind then Drule.asm_rl else
   1.158         if coind then
   1.159 @@ -748,7 +750,7 @@
   1.160               (rewrite_tac [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq] THEN
   1.161                 fold_tac rec_preds_defs) (mono RS (fp_def RS def_coinduct)))))
   1.162         else
   1.163 -         prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def
   1.164 +         prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
   1.165             rec_preds_defs ctxt1);
   1.166  
   1.167      val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind
   1.168 @@ -771,7 +773,8 @@
   1.169  
   1.170  (* external interfaces *)
   1.171  
   1.172 -fun gen_add_inductive_i mk_def (flags as {verbose, kind, alt_name, coind, no_elim, no_ind})
   1.173 +fun gen_add_inductive_i mk_def
   1.174 +    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind})
   1.175      cnames_syn pnames spec monos lthy =
   1.176    let
   1.177      val thy = ProofContext.theory_of lthy;
   1.178 @@ -835,7 +838,7 @@
   1.179      val (cs, ps) = chop (length cnames_syn) vars;
   1.180      val intrs = map (apsnd the_single) specs;
   1.181      val monos = Attrib.eval_thms lthy raw_monos;
   1.182 -    val flags = {verbose = verbose, kind = Thm.theoremK, alt_name = "",
   1.183 +    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK, alt_name = "",
   1.184        coind = coind, no_elim = false, no_ind = false};
   1.185    in
   1.186      lthy

     2.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 29 13:03:07 2008 +0100
     2.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 29 13:03:08 2008 +0100
     2.3 @@ -350,7 +350,7 @@
     2.4  
     2.5      val (ind_info, thy3') = thy2 |>
     2.6        InductivePackage.add_inductive_global (serial_string ())
     2.7 -        {verbose = false, kind = Thm.theoremK, alt_name = "",
     2.8 +        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = "",
     2.9            coind = false, no_elim = false, no_ind = false}
    2.10          rlzpreds rlzparams (map (fn (rintr, intr) =>
    2.11            ((Sign.base_name (name_of_thm intr), []),

     3.1 --- a/src/HOL/Tools/record_package.ML	Sat Mar 29 13:03:07 2008 +0100
     3.2 +++ b/src/HOL/Tools/record_package.ML	Sat Mar 29 13:03:08 2008 +0100
     3.3 @@ -24,7 +24,6 @@
     3.4  signature RECORD_PACKAGE =
     3.5  sig
     3.6    include BASIC_RECORD_PACKAGE
     3.7 -  val quiet_mode: bool ref
     3.8    val timing: bool ref
     3.9    val record_quick_and_dirty_sensitive: bool ref
    3.10    val updateN: string
    3.11 @@ -44,9 +43,9 @@
    3.12    val get_extinjects: theory -> thm list
    3.13    val get_simpset: theory -> simpset
    3.14    val print_records: theory -> unit
    3.15 -  val add_record: string list * string -> string option -> (string * string * mixfix) list
    3.16 +  val add_record: bool -> string list * string -> string option -> (string * string * mixfix) list
    3.17      -> theory -> theory
    3.18 -  val add_record_i: string list * string -> (typ list * string) option
    3.19 +  val add_record_i: bool -> string list * string -> (typ list * string) option
    3.20      -> (string * typ * mixfix) list -> theory -> theory
    3.21    val setup: theory -> theory
    3.22  end;
    3.23 @@ -107,9 +106,6 @@
    3.24  
    3.25  (* messages *)
    3.26  
    3.27 -val quiet_mode = ref false;
    3.28 -fun message s = if ! quiet_mode then () else writeln s;
    3.29 -
    3.30  fun trace_thm str thm =
    3.31      tracing (str ^ (Pretty.string_of (Display.pretty_thm thm)));
    3.32  
    3.33 @@ -2212,10 +2208,10 @@
    3.34  
    3.35  (*we do all preparations and error checks here, deferring the real
    3.36    work to record_definition*)
    3.37 -fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
    3.38 +fun gen_add_record prep_typ prep_raw_parent quiet_mode (params, bname) raw_parent raw_fields thy =
    3.39    let
    3.40      val _ = Theory.requires thy "Record" "record definitions";
    3.41 -    val _ = message ("Defining record " ^ quote bname ^ " ...");
    3.42 +    val _ = if quiet_mode then () else writeln ("Defining record " ^ quote bname ^ " ...");
    3.43  
    3.44  
    3.45      (* parents *)
    3.46 @@ -2312,7 +2308,7 @@
    3.47  
    3.48  val _ =
    3.49    OuterSyntax.command "record" "define extensible record" K.thy_decl
    3.50 -    (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
    3.51 +    (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record false x y z)));
    3.52  
    3.53  end;
    3.54