diff -r 83584916b6d7 -r 231b6d8231c6 src/Pure/ex/Guess.thy --- 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 =>