src/Pure/meta_simplifier.ML
changeset 14330 eb8b8241ef5b
parent 14242 ec70653a02bf
child 14643 130076a81b84
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Dec 25 22:48:32 2003 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Dec 25 23:18:04 2003 +0100
     1.3 @@ -940,7 +940,8 @@
     1.4  fun rewrite_cterm mode prover mss ct =
     1.5    let val {sign, t, maxidx, ...} = rep_cterm ct
     1.6        val Mss{depth, ...} = mss
     1.7 -  in simp_depth := depth;
     1.8 +  in trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
     1.9 +     simp_depth := depth;
    1.10       bottomc (mode, prover, sign, maxidx) mss ct
    1.11    end
    1.12    handle THM (s, _, thms) =>