src/Pure/ex/Guess.thy

         |> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts)
       end;
 
     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 =>
         Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
           (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)));