--- a/src/Pure/Isar/proof_context.ML Wed Nov 12 10:58:23 2003 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Nov 14 14:35:55 2003 +0100
@@ -29,7 +29,7 @@
val cert_typ_no_norm: context -> typ -> typ
val get_skolem: context -> string -> string
val extern_skolem: context -> term -> term
- val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
+ val read_termTs: string list -> context -> (string * typ) list -> term list * (indexname * typ) list
val read_termTs_env: (indexname -> typ option) * (indexname -> sort option) * string list -> context -> (string * typ) list -> term list * (indexname * typ) list
val read_term: context -> string -> term
val read_prop: context -> string -> term
@@ -591,8 +591,10 @@
end
in
-val read_termTs =
- gen_read (read_def_termTs false) (apfst o map) None false false false false;
+(* For where attribute:
+ Type vars generated by read will be distinct from those in "used". *)
+fun read_termTs used =
+ gen_read (read_def_termTs false) (apfst o map) (Some (K None, K None, used)) false false false false;
(* For rule_tac:
takes extra environment (types, sorts and used type vars) *)
fun read_termTs_env env =