removed dead code -- ctxt is never visible (see also 658fcba35ed7);
authorwenzelm
Thu Dec 12 14:35:31 2013 +0100 (2013-12-12)
changeset 54724b92694e756b8
parent 54723 124432e77ecf
child 54725 fc384e0a7f51
removed dead code -- ctxt is never visible (see also 658fcba35ed7);
src/Pure/raw_simplifier.ML
     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;