diff -r a3793600cb93 -r 4d3527b94f2a src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Pure/Isar/obtain.ML	Sun Dec 13 21:56:15 2015 +0100
@@ -266,7 +266,7 @@
     val ((thesis_var, thesis), thesis_ctxt) = obtain_thesis ctxt;
     val st = Goal.init (Thm.cterm_of ctxt thesis);
     val rule =
-      (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of
+      (case SINGLE (Method.insert_tac thesis_ctxt facts 1 THEN tac thesis_ctxt) st of
         NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
       | SOME th =>
           check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th)));
@@ -413,9 +413,8 @@
       (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)))
-    |> Seq.hd
+    |> Proof.refine_singleton
+        (Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis)))
   end;
 
 in