diff -r c0e1c121c7c0 -r 51a6997b1384 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Mon Jun 22 20:36:33 2015 +0200
@@ -159,7 +159,7 @@
     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
@@ -233,7 +233,7 @@
       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
@@ -409,7 +409,7 @@
     |> 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