# HG changeset patch
# User haftmann
# Date 1160571085 -7200
# Node ID 2a29a21825d16f26c8eb59ef4a00b36a54326f40
# Parent  0b8e436ed071e0b91e364e09b55158dcb7cafbce
slight type signature changes

diff -r 0b8e436ed071 -r 2a29a21825d1 src/FOL/hypsubstdata.ML
--- a/src/FOL/hypsubstdata.ML	Wed Oct 11 14:51:24 2006 +0200
+++ b/src/FOL/hypsubstdata.ML	Wed Oct 11 14:51:25 2006 +0200
@@ -1,10 +1,9 @@
 
 (** Applying HypsubstFun to generate hyp_subst_tac **)
 structure Hypsubst_Data =
-  struct
+struct
   structure Simplifier = Simplifier
-    (*These destructors  Match!*)
-  fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
+  fun dest_eq (Const("op =",T) $ t $ u) = ((t, u), domain_type T)
   val dest_Trueprop = FOLogic.dest_Trueprop
   val dest_imp = FOLogic.dest_imp
   val eq_reflection = eq_reflection
@@ -13,9 +12,8 @@
   val rev_mp = rev_mp
   val subst = subst
   val sym = sym
-  val thin_refl = prove_goal (the_context ())
-                  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
-  end;
+  val thin_refl = prove_goal (the_context ()) "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
+end;
 
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
 open Hypsubst;
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