hyp_subst_tac checks if the equality has type variables and uses a suitable
method if so. Affects the dest_eq function

--- a/src/FOL/ROOT.ML	Thu Nov 06 10:28:20 1997 +0100
+++ b/src/FOL/ROOT.ML	Thu Nov 06 10:29:37 1997 +0100
@@ -27,7 +27,8 @@
   struct
   structure Simplifier = Simplifier
     (*Take apart an equality judgement; otherwise raise Match!*)
-  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u)
+  fun dest_eq (Const("Trueprop",_) $ (Const("op =",T)  $ t $ u)) = 
+	(t, u, domain_type T)
   val eq_reflection = eq_reflection
   val imp_intr = impI
   val rev_mp = rev_mp

--- a/src/HOL/cladata.ML	Thu Nov 06 10:28:20 1997 +0100
+++ b/src/HOL/cladata.ML	Thu Nov 06 10:29:37 1997 +0100
@@ -14,7 +14,8 @@
   struct
   structure Simplifier = Simplifier
   (*Take apart an equality judgement; otherwise raise Match!*)
-  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
+  fun dest_eq (Const("Trueprop",_) $ (Const("op =",T)  $ t $ u)) = 
+	(t, u, domain_type T)
   val eq_reflection = eq_reflection
   val imp_intr = impI
   val rev_mp = rev_mp

--- 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