--- a/src/Pure/Isar/obtain.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/obtain.ML Sat Jan 21 23:02:14 2006 +0100
@@ -40,7 +40,7 @@
((string * Attrib.src list) * (string * (string list * string list)) list) list
-> bool -> Proof.state -> Proof.state
val obtain_i: (string * typ option) list ->
- ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
+ ((string * attribute list) * (term * (term list * term list)) list) list
-> bool -> Proof.state -> Proof.state
val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
@@ -137,7 +137,7 @@
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
|> Proof.fix_i [(thesisN, NONE)]
|> Proof.assume_i
- [((thatN, [Attrib.context (ContextRules.intro_query NONE)]), [(that_prop, ([], []))])]
+ [((thatN, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
@@ -146,7 +146,7 @@
in
-val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp;
+val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
end;