src/Pure/tactical.ML
changeset 82590 d08f5b5ead0a
parent 76051 854e9223767f
--- a/src/Pure/tactical.ML	Fri Apr 25 16:54:39 2025 +0200
+++ b/src/Pure/tactical.ML	Fri Apr 25 18:06:12 2025 +0200
@@ -176,7 +176,7 @@
 
 (*Print the current proof state and pass it on.*)
 fun print_tac ctxt msg st =
-  (tracing (msg ^ "\n" ^ Goal_Display.string_of_goal ctxt st); Seq.single st);
+  (tracing (Goal_Display.print_goal ctxt msg st); Seq.single st);
 
 
 (*Deterministic REPEAT: only retains the first outcome;