src/Pure/Isar/obtain.ML

     state
     |> Proof.have 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
-    |> (fn state' => state'
-        |> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
+    |-> Proof.refine_insert
   end;
 
 in
 
 val consider = gen_consider cert_obtains;

     state
     |> Proof.have NONE after_qed
       [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
       [((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
       [(Thm.empty_binding, [(thesis, [])])] int
-    |> (fn state' => state'
-        |> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
+    |-> Proof.refine_insert
     |> Proof.map_context (fold Variable.bind_term binds')
   end;
 
 in
 

     |> 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"
-      (SOME before_qed) after_qed [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
+      (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
+        Goal.init (Thm.cterm_of ctxt thesis)))
+    |> Seq.hd
   end;
 
 in
 
 val guess = gen_guess Proof_Context.cert_var;