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;