diff -r 0b8e436ed071 -r 2a29a21825d1 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Wed Oct 11 14:51:24 2006 +0200
+++ b/src/Provers/hypsubst.ML	Wed Oct 11 14:51:25 2006 +0200
@@ -34,8 +34,8 @@
 signature HYPSUBST_DATA =
   sig
   val dest_Trueprop    : term -> term
-  val dest_eq          : term -> term*term*typ
-  val dest_imp         : term -> term*term
+  val dest_eq          : term -> (term * term) *typ
+  val dest_imp         : term -> term * term
   val eq_reflection    : thm               (* a=b ==> a==b *)
   val rev_eq_reflection: thm               (* a==b ==> a=b *)
   val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
@@ -55,7 +55,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 * typ -> bool
+  val inspect_pair           : bool -> bool -> (term * term) * typ -> bool
   val mk_eqs                 : bool -> thm -> thm list
   val stac                   : thm -> int -> tactic
   val hypsubst_setup         : theory -> theory
@@ -89,7 +89,7 @@
         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,T) =
+fun inspect_pair bnd novars ((t, u), T) =
   if novars andalso maxidx_of_typ T <> ~1
   then raise Match   (*variables in the type!*)
   else