dropped debug message
authorhaftmann
Wed, 03 Nov 2010 14:14:06 +0100
changeset 40353 2f44afc0fff3
parent 40352 8fd36f8a5cb7
child 40354 d7dfec07806a
dropped debug message
src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Wed Nov 03 14:14:06 2010 +0100
+++ b/src/HOL/Tools/primrec.ML	Wed Nov 03 14:14:06 2010 +0100
@@ -31,8 +31,6 @@
 fun primrec_error msg = raise PrimrecError (msg, NONE);
 fun primrec_error_eqn msg eqn = raise PrimrecError (msg, SOME eqn);
 
-fun message s = if ! Toplevel.debug then tracing s else ();
-
 
 (* preprocessing of equations *)
 
@@ -251,7 +249,6 @@
           if Variable.is_fixed lthy x then I else insert (op =) x | _ => I) eqs [];
         val rewrites = rec_rewrites' @ map (snd o snd) defs;
         fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
-        val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
       in map (fn eq => Goal.prove lthy frees [] eq tac) eqs end;
   in ((prefix, (fs, defs)), prove) end
   handle PrimrecError (msg, some_eqn) =>