src/Pure/Isar/obtain.ML

 *)
 
 signature OBTAIN =
 sig
   val obtain: ((string list * string option) * Comment.text) list
-    * ((string * Args.src list * (string * (string list * string list)) 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)
+    * (((string * Proof.context attribute list) * (term * (term list * term list)) list)
       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
 end;
 
 structure Obtain: OBTAIN =
 struct

 
 fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
   let
     val _ = Proof.assert_forward_or_chain state;
     val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
+    val thy = Proof.theory_of state;
 
     (*obtain vars*)
     val (vars_ctxt, vars) =
       foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
     val xs = flat (map fst vars);

     val bind_skolem = ProofContext.bind_skolem vars_ctxt (xs @ [thesisN]);
     fun bind_propp (prop, (pats1, pats2)) =
       (bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2));
 
     (*obtain asms*)
-    fun prep_asm (ctxt, (name, src, raw_propps)) =
-      let
-        val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
-        val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
-      in (ctxt', ((name, atts, map bind_propp propps), map #1 propps)) end;
+    val (asms_ctxt, proppss) = prep_propp (vars_ctxt, map (snd o Comment.ignore) raw_asms);
+    val asm_props = flat (map (map fst) proppss);
 
-    val (asms_ctxt, asms_result) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
-    val (asms, asm_propss) = Library.split_list asms_result;
-    val asm_props = flat asm_propss;
+    fun prep_asm ((name, src), propps) = ((name, map (prep_att thy) src), map bind_propp propps);
+    val asms = map2 prep_asm (map (fst o Comment.ignore) raw_asms, proppss);
+
     val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
 
     (*that_prop*)
     fun find_free x t =
       (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
     fun occs_var x = Library.get_first (find_free x) asm_props;
     val xs' = mapfilter occs_var xs;
     val parms = map (bind_skolem o Free) xs';
 
-    val bound_thesis = bind_skolem (AutoBind.atomic_judgment (Proof.theory_of state) thesisN);
+    val bound_thesis = bind_skolem (AutoBind.atomic_judgment thy thesisN);
     val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
 
     fun export_obtained rule =
       (disch_obtained state parms rule, fn _ => fn _ => []);
 

   in
     state
     |> Proof.enter_forward
     |> Proof.begin_block
     |> Proof.fix_i [([thesisN], None)]
-    |> Proof.assume_i [(thatN, [Method.intro_local], [(that_prop, ([], []))])]
+    |> 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')))))

   OuterSyntax.command "obtain" "generalized existence"
     K.prf_asm_goal
     (Scan.optional
       (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
         --| P.$$$ "where") [] --
-      P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
+      P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment)
     >> (Toplevel.print oo (Toplevel.proof o obtain)));
 
 val _ = OuterSyntax.add_keywords ["where"];
 val _ = OuterSyntax.add_parsers [obtainP];