src/Pure/Isar/obtain.ML
changeset 16842 5979c46853d1
parent 16787 b6b6e2faaa41
child 17034 b4d9b87c102e
--- a/src/Pure/Isar/obtain.ML	Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Jul 14 19:28:24 2005 +0200
@@ -118,11 +118,10 @@
     |> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
     |> Proof.fix_i [([thesisN], NONE)]
     |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
-    |> (fn state' =>
-        state'
-        |> Proof.from_facts chain_facts
-        |> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
-        |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
+    |> `Proof.the_facts
+    ||> Proof.from_facts chain_facts
+    ||> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
+    |-> (fn facts => Method.refine (Method.Basic (K (Method.insert facts))))
   end;
 
 val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;