src/Pure/Isar/obtain.ML

         |> Proof.bind_terms Auto_Bind.no_facts
       end;
 
     val goal = Var (("guess", 0), propT);
     fun print_result ctxt' (k, [(s, [_, th])]) =
-      Proof_Display.print_results Isabelle_Markup.state int ctxt' (k, [(s, [th])]);
+      Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
     val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
         (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
     fun after_qed [[_, res]] =
       Proof.end_block #> guess_context (check_result ctxt thesis res);
   in