# HG changeset patch
# User wenzelm
# Date 1662239438 -7200
# Node ID 854e9223767f633ec8d0b0b45e8cc17925f76c91
# Parent  f1dc3d9d5164e154ee3ca32c8b1db0f9f06a38a0
tuned signature;

diff -r f1dc3d9d5164 -r 854e9223767f src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML	Sat Sep 03 22:25:22 2022 +0200
+++ b/src/HOL/Library/conditional_parametricity.ML	Sat Sep 03 23:10:38 2022 +0200
@@ -110,8 +110,7 @@
 (* Tactics  *)
 (* helper tactics for printing *)
 fun error_tac ctxt msg st =
-  (error(msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
-  Seq.single st);
+  (error (msg ^ "\n" ^ Goal_Display.string_of_goal ctxt st); Seq.single st);
 
 fun error_tac' ctxt msg = SELECT_GOAL (error_tac ctxt msg);
 
diff -r f1dc3d9d5164 -r 854e9223767f src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Sep 03 22:25:22 2022 +0200
+++ b/src/Pure/goal.ML	Sat Sep 03 23:10:38 2022 +0200
@@ -80,8 +80,7 @@
 *)
 fun check_finished ctxt th =
   if Thm.no_prems th then th
-  else
-    raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]);
+  else raise THM ("Proof failed.\n" ^ Goal_Display.string_of_goal ctxt th, 0, [th]);
 
 fun finish ctxt = check_finished ctxt #> conclude;
 
diff -r f1dc3d9d5164 -r 854e9223767f src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Sat Sep 03 22:25:22 2022 +0200
+++ b/src/Pure/tactical.ML	Sat Sep 03 23:10:38 2022 +0200
@@ -176,8 +176,7 @@
 
 (*Print the current proof state and pass it on.*)
 fun print_tac ctxt msg st =
- (tracing (msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
-  Seq.single st);
+  (tracing (msg ^ "\n" ^ Goal_Display.string_of_goal ctxt st); Seq.single st);
 
 
 (*Deterministic REPEAT: only retains the first outcome;