src/Pure/Isar/obtain.ML

--- a/src/Pure/Isar/obtain.ML	Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Jun 09 16:07:11 2015 +0200
@@ -155,7 +155,7 @@
   in
     state
     |> Proof.enter_forward
-    |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
+    |> Proof.have NONE (K I) [] [(Thm.empty_binding, [(obtain_prop, [])])] int
     |> Proof.map_context (fold Variable.bind_term binds')
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
@@ -163,7 +163,7 @@
       [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
-    ||> Proof.show NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
+    ||> Proof.show NONE after_qed [] [(Thm.empty_binding, [(thesis, [])])] false
     |-> Proof.refine_insert
   end;
 
@@ -314,8 +314,8 @@
     |> Proof.begin_block
     |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
-    |> Proof.local_goal print_result (K I) (K (rpair []))
-      "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
+    |> Proof.internal_goal print_result Proof_Context.mode_schematic "guess"
+      (SOME before_qed) after_qed [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
     |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
         Goal.init (Thm.cterm_of ctxt thesis))) |> Seq.hd
   end;