src/Pure/Isar/obtain.ML
changeset 18728 6790126ab5f6
parent 18693 8ae076ee5e19
child 18769 e90eb0bc0ddd
     1.1 --- a/src/Pure/Isar/obtain.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -40,7 +40,7 @@
     1.4      ((string * Attrib.src list) * (string * (string list * string list)) list) list
     1.5      -> bool -> Proof.state -> Proof.state
     1.6    val obtain_i: (string * typ option) list ->
     1.7 -    ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
     1.8 +    ((string * attribute list) * (term * (term list * term list)) list) list
     1.9      -> bool -> Proof.state -> Proof.state
    1.10    val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
    1.11    val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
    1.12 @@ -137,7 +137,7 @@
    1.13      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    1.14      |> Proof.fix_i [(thesisN, NONE)]
    1.15      |> Proof.assume_i
    1.16 -      [((thatN, [Attrib.context (ContextRules.intro_query NONE)]), [(that_prop, ([], []))])]
    1.17 +      [((thatN, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
    1.18      |> `Proof.the_facts
    1.19      ||> Proof.chain_facts chain_facts
    1.20      ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
    1.21 @@ -146,7 +146,7 @@
    1.22  
    1.23  in
    1.24  
    1.25 -val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp;
    1.26 +val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
    1.27  val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
    1.28  
    1.29  end;