src/Pure/Isar/obtain.ML
changeset 11890 28e42a90bea8
parent 11816 545aab7410ac
child 12055 a9c44895cc8c
     1.1 --- a/src/Pure/Isar/obtain.ML	Mon Oct 22 18:02:21 2001 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Mon Oct 22 18:02:50 2001 +0200
     1.3 @@ -20,12 +20,12 @@
     1.4  
     1.5  signature OBTAIN =
     1.6  sig
     1.7 -  val obtain: ((string list * string option) * Comment.text) 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 -      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.13 +  val obtain: (string list * string option) list ->
    1.14 +    ((string * Proof.context attribute list) * (string * (string list * string list)) list) list
    1.15 +    -> Proof.state -> Proof.state Seq.seq
    1.16 +  val obtain_i: (string list * typ option) list ->
    1.17 +    ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
    1.18 +    -> Proof.state -> Proof.state Seq.seq
    1.19  end;
    1.20  
    1.21  structure Obtain: OBTAIN =
    1.22 @@ -62,7 +62,7 @@
    1.23  
    1.24  val thatN = "that";
    1.25  
    1.26 -fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
    1.27 +fun gen_obtain prep_vars prep_propp raw_vars raw_asms state =
    1.28    let
    1.29      val _ = Proof.assert_forward_or_chain state;
    1.30      val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
    1.31 @@ -70,17 +70,14 @@
    1.32      val sign = Theory.sign_of thy;
    1.33  
    1.34      (*obtain vars*)
    1.35 -    val (vars_ctxt, vars) =
    1.36 -      foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
    1.37 +    val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, raw_vars);
    1.38      val xs = flat (map fst vars);
    1.39      val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;
    1.40  
    1.41      (*obtain asms*)
    1.42 -    val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map (snd o Comment.ignore) raw_asms);
    1.43 +    val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    1.44      val asm_props = flat (map (map fst) proppss);
    1.45 -
    1.46 -    fun prep_asm ((name, src), propps) = ((name, map (prep_att thy) src), propps);
    1.47 -    val asms = map2 prep_asm (map (fst o Comment.ignore) raw_asms, proppss);
    1.48 +    val asms = map fst raw_asms ~~ proppss;
    1.49  
    1.50      val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
    1.51  
    1.52 @@ -118,31 +115,8 @@
    1.53        |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
    1.54    end;
    1.55  
    1.56 -
    1.57 -val obtain = ProofHistory.applys o
    1.58 -  (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
    1.59 -
    1.60 -val obtain_i = ProofHistory.applys o
    1.61 -  (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
    1.62 -
    1.63 +val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
    1.64 +val obtain_i = gen_obtain ProofContext.cert_vars ProofContext.cert_propp;
    1.65  
    1.66  
    1.67 -(** outer syntax **)
    1.68 -
    1.69 -local structure P = OuterParse and K = OuterSyntax.Keyword in
    1.70 -
    1.71 -val obtainP =
    1.72 -  OuterSyntax.command "obtain" "generalized existence"
    1.73 -    K.prf_asm_goal
    1.74 -    (Scan.optional
    1.75 -      (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
    1.76 -        --| P.$$$ "where") [] --
    1.77 -      P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment)
    1.78 -    >> (Toplevel.print oo (Toplevel.proof o obtain)));
    1.79 -
    1.80 -val _ = OuterSyntax.add_keywords ["where"];
    1.81 -val _ = OuterSyntax.add_parsers [obtainP];
    1.82 -
    1.83  end;
    1.84 -
    1.85 -end;