# HG changeset patch
# User wenzelm
# Date 1386855331 -3600
# Node ID b92694e756b807567888c4eb83b336a0c0b16b9d
# Parent  124432e77ecfc4006a7673e93e7cdf5ff234efed
removed dead code -- ctxt is never visible (see also 658fcba35ed7);

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