# HG changeset patch
# User wenzelm
# Date 973283226 -3600
# Node ID 93630e0c5ae958eebd3ee02cc4190f69c62a9eec
# Parent  98c95ebf804fa5eaf6071c7d8154dad35e6184c2
improved handling of "that": insert into goal, only declare as Pure "intro";
eliminated functor;

diff -r 98c95ebf804f -r 93630e0c5ae9 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Fri Nov 03 21:26:11 2000 +0100
+++ b/src/Pure/Isar/obtain.ML	Fri Nov 03 21:27:06 2000 +0100
@@ -12,18 +12,12 @@
   {
     fix thesis
     assume that: "!!x. P x ==> thesis"
-    <chain_facts> have thesis <proof>
+    <chain_facts> have thesis <proof (insert that)>
   }
-  fix x assm(obtained) "P x"
+  fix x assm (obtained) "P x"
 
 *)
 
-signature OBTAIN_DATA =
-sig
-  val atomic_thesis: string -> term
-  val that_atts: Proof.context attribute list
-end;
-
 signature OBTAIN =
 sig
   val obtain: ((string list * string option) * Comment.text) list
@@ -34,7 +28,7 @@
       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
 end;
 
-functor ObtainFun(Data: OBTAIN_DATA): OBTAIN =
+structure Obtain: OBTAIN =
 struct
 
 
@@ -58,7 +52,7 @@
       raise Proof.STATE ("Conclusion contains obtained parameters: " ^
         space_implode " " (map (Sign.string_of_term sign) bads), state)
     else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
-      raise Proof.STATE ("Conclusion is not an object-logic judgment", state)
+      raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
   end;
 
@@ -102,7 +96,7 @@
     val xs' = mapfilter occs_var xs;
     val parms = map (bind_skolem o Free) xs';
 
-    val bound_thesis = bind_skolem (Data.atomic_thesis thesisN);
+    val bound_thesis = bind_skolem (AutoBind.atomic_judgment (Proof.theory_of state) thesisN);
     val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
 
     fun export_obtained rule =
@@ -118,16 +112,19 @@
     |> Proof.enter_forward
     |> Proof.begin_block
     |> Proof.fix_i [([thesisN], None)]
-    |> Proof.assume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
-    |> Proof.from_facts chain_facts
-    |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
+    |> Proof.assume_i [(thatN, [Method.intro_local], [(that_prop, ([], []))])]
+    |> (fn state' =>
+      state'
+      |> Proof.from_facts chain_facts
+      |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
+      |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
   end;
 
 
-val obtain = ProofHistory.apply o
+val obtain = ProofHistory.applys o
   (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
 
-val obtain_i = ProofHistory.apply o
+val obtain_i = ProofHistory.applys o
   (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));