1.1 --- a/src/Pure/raw_simplifier.ML	Thu Dec 12 13:50:44 2013 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Thu Dec 12 14:35:31 2013 +0100
     1.3 @@ -1311,11 +1311,6 @@
     1.4        Theory.subthy (theory_of_cterm ct, thy) orelse
     1.5          raise CTERM ("rewrite_cterm: bad background theory", [ct]);
     1.6  
     1.7 -    val depth = simp_depth ctxt;
     1.8 -    val _ =
     1.9 -      if depth mod 20 = 0 then
    1.10 -        Context_Position.if_visible ctxt warning ("Simplification depth " ^ string_of_int depth)
    1.11 -      else ();
    1.12      val _ = trace_cterm ctxt false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ct;
    1.13      val _ = check_bounds ctxt ct;
    1.14    in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;