src/Pure/Isar/obtain.ML
changeset 10464 b7b916a82dca
parent 10379 93630e0c5ae9
child 10582 49ebade930ea
     1.1 --- a/src/Pure/Isar/obtain.ML	Mon Nov 13 21:59:49 2000 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Mon Nov 13 22:01:07 2000 +0100
     1.3 @@ -21,10 +21,10 @@
     1.4  signature OBTAIN =
     1.5  sig
     1.6    val obtain: ((string list * string option) * Comment.text) list
     1.7 -    * ((string * Args.src list * (string * (string list * string list)) list)
     1.8 +    * (((string * Args.src list) * (string * (string list * string list)) list)
     1.9        * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.10    val obtain_i: ((string list * typ option) * Comment.text) list
    1.11 -    * ((string * Proof.context attribute list * (term * (term list * term list)) list)
    1.12 +    * (((string * Proof.context attribute list) * (term * (term list * term list)) list)
    1.13        * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.14  end;
    1.15  
    1.16 @@ -66,6 +66,7 @@
    1.17    let
    1.18      val _ = Proof.assert_forward_or_chain state;
    1.19      val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
    1.20 +    val thy = Proof.theory_of state;
    1.21  
    1.22      (*obtain vars*)
    1.23      val (vars_ctxt, vars) =
    1.24 @@ -78,15 +79,12 @@
    1.25        (bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2));
    1.26  
    1.27      (*obtain asms*)
    1.28 -    fun prep_asm (ctxt, (name, src, raw_propps)) =
    1.29 -      let
    1.30 -        val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
    1.31 -        val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
    1.32 -      in (ctxt', ((name, atts, map bind_propp propps), map #1 propps)) end;
    1.33 +    val (asms_ctxt, proppss) = prep_propp (vars_ctxt, map (snd o Comment.ignore) raw_asms);
    1.34 +    val asm_props = flat (map (map fst) proppss);
    1.35  
    1.36 -    val (asms_ctxt, asms_result) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
    1.37 -    val (asms, asm_propss) = Library.split_list asms_result;
    1.38 -    val asm_props = flat asm_propss;
    1.39 +    fun prep_asm ((name, src), propps) = ((name, map (prep_att thy) src), map bind_propp propps);
    1.40 +    val asms = map2 prep_asm (map (fst o Comment.ignore) raw_asms, proppss);
    1.41 +
    1.42      val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
    1.43  
    1.44      (*that_prop*)
    1.45 @@ -96,7 +94,7 @@
    1.46      val xs' = mapfilter occs_var xs;
    1.47      val parms = map (bind_skolem o Free) xs';
    1.48  
    1.49 -    val bound_thesis = bind_skolem (AutoBind.atomic_judgment (Proof.theory_of state) thesisN);
    1.50 +    val bound_thesis = bind_skolem (AutoBind.atomic_judgment thy thesisN);
    1.51      val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
    1.52  
    1.53      fun export_obtained rule =
    1.54 @@ -112,7 +110,7 @@
    1.55      |> Proof.enter_forward
    1.56      |> Proof.begin_block
    1.57      |> Proof.fix_i [([thesisN], None)]
    1.58 -    |> Proof.assume_i [(thatN, [Method.intro_local], [(that_prop, ([], []))])]
    1.59 +    |> Proof.assume_i [((thatN, [Method.intro_local]), [(that_prop, ([], []))])]
    1.60      |> (fn state' =>
    1.61        state'
    1.62        |> Proof.from_facts chain_facts
    1.63 @@ -139,7 +137,7 @@
    1.64      (Scan.optional
    1.65        (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
    1.66          --| P.$$$ "where") [] --
    1.67 -      P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
    1.68 +      P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment)
    1.69      >> (Toplevel.print oo (Toplevel.proof o obtain)));
    1.70  
    1.71  val _ = OuterSyntax.add_keywords ["where"];