# HG changeset patch
# User nipkow
# Date 1072390684 -3600
# Node ID eb8b8241ef5b741d40e909298d086192f2b69664
# Parent  ff3210fe968fc469d45613e28ae5d83d97d1917f
Added trace msg

diff -r ff3210fe968f -r eb8b8241ef5b 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) =>