src/Pure/Isar/isar_thy.ML

     -> Toplevel.transition -> Toplevel.transition
   val finally: ((string * Args.src list) list * Comment.interest) option * Comment.text
     -> 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
   val parse_ast_translation: string -> theory -> theory
   val parse_translation: string -> theory -> theory

 val match_bind_i = ProofHistory.apply o Proof.match_bind_i o map Comment.ignore;
 
 
 (* 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 =
   ProofHistory.init (Toplevel.undo_limit int)
     (f name (map (Attrib.global_attribute thy) src) s thy);

   f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state));
 
 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);
 
 in
 

 fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x);
 
 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;
 fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text verb) txt);