--- a/src/Pure/ex/Guess.thy Fri Mar 21 18:37:05 2025 +0100
+++ b/src/Pure/ex/Guess.thy Fri Mar 21 22:26:18 2025 +0100
@@ -147,9 +147,8 @@
val guess = (("guess", 0), propT);
val goal = Var guess;
- val pos = Position.thread_data ();
fun print_result ctxt' (k, [(s, [_, th])]) =
- Proof_Display.print_results {interactive = int, pos = pos, proof_state = true}
+ Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}
ctxt' (k, [(s, [th])]);
val before_qed =
Method.primitive_text (fn ctxt =>