diff -r e64ff1c1bc70 -r cc4b6791d5dc src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Thu Nov 06 10:28:20 1997 +0100
+++ b/src/Provers/hypsubst.ML	Thu Nov 06 10:29:37 1997 +0100
@@ -25,7 +25,7 @@
 signature HYPSUBST_DATA =
   sig
   structure Simplifier : SIMPLIFIER
-  val dest_eq	       : term -> term*term
+  val dest_eq	       : term -> term*term*typ
   val eq_reflection    : thm		   (* a=b ==> a==b *)
   val imp_intr	       : thm		   (* (P ==> Q) ==> P-->Q *)
   val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
@@ -42,7 +42,7 @@
   val gen_hyp_subst_tac      : bool -> int -> tactic
   val vars_gen_hyp_subst_tac : bool -> int -> tactic
   val eq_var                 : bool -> bool -> term -> int * bool
-  val inspect_pair           : bool -> bool -> term * term -> bool
+  val inspect_pair           : bool -> bool -> term * term * typ -> bool
   val mk_eqs                 : thm -> thm list
   val thin_leading_eqs_tac   : bool -> int -> int -> tactic
   end;
@@ -81,7 +81,10 @@
         but we can't check for this -- hence bnd and bound_hyp_subst_tac
   Prefer to eliminate Bound variables if possible.
   Result:  true = use as is,  false = reorient first *)
-fun inspect_pair bnd novars (t,u) =
+fun inspect_pair bnd novars (t,u,T) =
+  if novars andalso maxidx_of_typ T <> ~1 
+  then raise Match   (*variables in the type!*)
+  else
   case (contract t, contract u) of
        (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
 		       then raise Match