src/HOL/Tools/old_primrec_package.ML
changeset 26478 9d1029ce0e13
parent 25561 d955e1d01e6a
child 26939 1035c89b4c02
--- a/src/HOL/Tools/old_primrec_package.ML	Sat Mar 29 13:03:08 2008 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Sat Mar 29 13:03:09 2008 +0100
@@ -7,7 +7,6 @@
 
 signature OLD_PRIMREC_PACKAGE =
 sig
-  val quiet_mode: bool ref
   val unify_consts: theory -> term list -> term list -> term list * term list
   val add_primrec: string -> ((bstring * string) * Attrib.src list) list
     -> theory -> thm list * theory
@@ -31,12 +30,6 @@
   primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
 
 
-(* messages *)
-
-val quiet_mode = ref false;
-fun message s = if ! quiet_mode then () else writeln s;
-
-
 (*the following code ensures that each recursive set always has the
   same type in all introduction rules*)
 fun unify_consts thy cs intr_ts =
@@ -283,8 +276,6 @@
       |> Sign.add_path primrec_name
       |> fold_map def (map (fn (name, t) => ((name, []), t)) defs');
     val rewrites = (map mk_meta_eq rec_rewrites) @ map snd defs_thms';
-    val _ = message ("Proving equations for primrec function(s) " ^
-      commas_quote (map fst nameTs1) ^ " ...");
     val simps = map (fn (_, t) => Goal.prove_global thy' [] [] t
         (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
     val (simps', thy'') =