src/Pure/Isar/obtain.ML

     val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt;
     val obtains = prep_obtains thesis_ctxt thesis raw_obtains;
     val atts = Rule_Cases.cases_open :: obtains_attributes raw_obtains;
   in
     state
-    |> Proof.have NONE (K I)
+    |> Proof.have true NONE (K I)
       [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
       (map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
       [((Binding.empty, atts), [(thesis, [])])] int
     |-> Proof.refine_insert
   end;

         |> Proof.map_context declare_asms
         |> Proof.assm (obtain_export params_ctxt rule cparams) asms
       end;
   in
     state
-    |> Proof.have NONE after_qed
+    |> Proof.have true NONE after_qed
       [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
       [((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
       [(Thm.empty_binding, [(thesis, [])])] int
     |-> Proof.refine_insert
     |> Proof.map_context (fold Variable.bind_term binds')

     state
     |> Proof.enter_forward
     |> Proof.begin_block
     |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
-    |> Proof.internal_goal print_result Proof_Context.mode_schematic "guess"
+    |> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess"
       (SOME before_qed) after_qed
       [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
     |> snd
     |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
         Goal.init (Thm.cterm_of ctxt thesis)))