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;