src/Provers/hypsubst.ML

           val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
           (*omit selected equality, returning other hyps*)
           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,
                    REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
                    etac (if symopt then ssubst else Data.subst) i,