# HG changeset patch
# User nipkow
# Date 757674573 -3600
# Node ID feb8ff35810a693fa08594853ce765963d5470ca
# Parent  342f88d2e8abaa9230b86929354db5e6f1283992
changed tracing of simplifier

diff -r 342f88d2e8ab -r feb8ff35810a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Jan 02 15:10:36 1994 +0100
+++ b/src/Pure/thm.ML	Tue Jan 04 10:09:33 1994 +0100
@@ -804,6 +804,12 @@
 
 fun prtm a sg t = (writeln a; writeln(Sign.string_of_term sg t));
 
+val trace_simp = ref false;
+
+fun trace_term a sg t = if !trace_simp then prtm a sg t else ();
+
+fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
+
 (*simple test for looping rewrite*)
 fun loops sign prems (lhs,rhs) =
   null(prems) andalso
@@ -829,11 +835,12 @@
   case mk_rrule thm of
     None => mss
   | Some(rrule as {lhs,...}) =>
-      Mss{net= (Net.insert_term((lhs,rrule),net,eq)
-                handle Net.INSERT =>
+      (trace_thm "Adding rewrite rule:" thm;
+       Mss{net= (Net.insert_term((lhs,rrule),net,eq)
+                 handle Net.INSERT =>
                   (prtm "Warning: ignoring duplicate rewrite rule" sign prop;
                    net)),
-          congs=congs, primes=primes, prems=prems,mk_rews=mk_rews};
+           congs=congs, primes=primes, prems=prems,mk_rews=mk_rews});
 
 fun del_simp(mss as Mss{net,congs,primes,prems,mk_rews},
              thm as Thm{sign,prop,...}) =
@@ -884,12 +891,6 @@
 type termrec = (Sign.sg * term list) * term;
 type conv = meta_simpset -> termrec -> termrec;
 
-val trace_simp = ref false;
-
-fun trace_term a sg t = if !trace_simp then prtm a sg t else ();
-
-fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
-
 fun check_conv(thm as Thm{hyps,prop,...}, prop0) =
   let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; None)
       val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
@@ -992,7 +993,6 @@
               if maxidx_of_term s' <> ~1 then ([],mss)
               else let val thm = Thm{sign=sign,hyps=[s'],prop=s',maxidx= ~1}
                    in (mk_rews thm, add_prems(mss,[thm])) end
-            val unit = seq (trace_thm "Adding rewrite rule:") rthms
             val mss' = add_simps(mss,rthms)
             val (hyps2,u') = botc mss' (hyps1,u)
             val hyps2' = if s' mem hyps1 then hyps2 else hyps2\s'