src/Pure/meta_simplifier.ML

--- a/src/Pure/meta_simplifier.ML	Thu Dec 25 22:48:32 2003 +0100
+++ b/src/Pure/meta_simplifier.ML	Thu Dec 25 23:18:04 2003 +0100
@@ -940,7 +940,8 @@
 fun rewrite_cterm mode prover mss ct =
   let val {sign, t, maxidx, ...} = rep_cterm ct
       val Mss{depth, ...} = mss
-  in simp_depth := depth;
+  in trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
+     simp_depth := depth;
      bottomc (mode, prover, sign, maxidx) mss ct
   end
   handle THM (s, _, thms) =>