src/Pure/Isar/isar_thy.ML

--- a/src/Pure/Isar/isar_thy.ML	Fri Oct 01 20:38:16 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Fri Oct 01 20:38:50 1999 +0200
@@ -135,6 +135,12 @@
     -> Toplevel.transition -> Toplevel.transition
   val finally_i: (thm list * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
+  val obtain: ((string list * string option) * Comment.text) list
+    * ((string * Args.src list * (string * (string list * string list)) list)
+      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val obtain_i: ((string list * typ option) * Comment.text) list
+    * ((string * Proof.context attribute list * (term * (term list * term list)) list)
+      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val use_mltext: string -> bool -> theory option -> unit
   val use_mltext_theory: string -> bool -> theory -> theory
   val use_setup: string -> theory -> theory
@@ -281,6 +287,9 @@
 
 (* statements *)
 
+fun multi_local_attribute state (name, src, s) =
+  (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s);
+
 local
 
 fun global_statement f (name, src, s) int thy =
@@ -296,8 +305,7 @@
 fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
 
 fun multi_statement f args = ProofHistory.apply (fn state =>
-  f (map (fn (name, src, s) =>
-      (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s)) args) state);
+  f (map (multi_local_attribute state) args) state);
 
 fun multi_statement_i f args = ProofHistory.apply (f args);
 
@@ -433,6 +441,17 @@
 end;
 
 
+(* obtain *)
+
+fun obtain (xs, asms) = ProofHistory.applys (fn state =>
+  Obtain.obtain (map Comment.ignore xs)
+    (map (multi_local_attribute state o Comment.ignore) asms) state);
+
+fun obtain_i (xs, asms) = ProofHistory.applys
+  (Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms));
+
+
+
 (* use ML text *)
 
 fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text verb) txt;