src/Provers/hypsubst.ML
changeset 12262 11ff5f47df6e
parent 10821 dcb75538f542
child 12377 c1e3e7d3f469
--- a/src/Provers/hypsubst.ML	Wed Nov 21 00:35:13 2001 +0100
+++ b/src/Provers/hypsubst.ML	Wed Nov 21 00:36:51 2001 +0100
@@ -236,7 +236,7 @@
           val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
           val n = length hyps
       in
-         if !trace then writeln "Substituting an equality" else ();
+         if !trace then tracing "Substituting an equality" else ();
          DETERM
            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
                    rotate_tac 1 i,