diff -r 33e5ef9a4c98 -r a7ef3f7588c5 src/Pure/Isar/proof_context.ML
--- 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 =