# HG changeset patch
# User ballarin
# Date 1038576415 -3600
# Node ID d48d1716bb6d0d7b2853c6aa443585e8b5aacfd5
# Parent  e564c3d2d174996f1b661bcd7e64a10936a35e55
Incompatibility with SML/NJ fixed.

diff -r e564c3d2d174 -r d48d1716bb6d src/HOL/Algebra/abstract/order.ML
--- a/src/HOL/Algebra/abstract/order.ML	Fri Nov 29 09:48:28 2002 +0100
+++ b/src/HOL/Algebra/abstract/order.ML	Fri Nov 29 14:26:55 2002 +0100
@@ -49,12 +49,12 @@
 
 (* Compares two terms, ignoring type information. *)
 infix e;
-fun Const (s1, _)   e Const (s2, _)   = s1 = s2
-  | Free (s1, _)    e Free (s2, _)    = s1 = s2
-  | Var (ix1, _)    e Var (ix2, _)    = ix1 = ix2
-  | Bound i1        e Bound i2        = i1 = i2
-  | Abs (s1, _, t1) e Abs (s2, _, t2) = s1 = s2 andalso t1 = t2
-  | (s1 $ s2)       e (t1 $ t2)       = s1 = t1 andalso s2 = t2
+fun (Const (s1, _))   e (Const (s2, _))   = s1 = s2
+  | (Free (s1, _))    e (Free (s2, _))    = s1 = s2
+  | (Var (ix1, _))    e (Var (ix2, _))    = ix1 = ix2
+  | (Bound i1)        e (Bound i2)        = i1 = i2
+  | (Abs (s1, _, t1)) e (Abs (s2, _, t2)) = s1 = s2 andalso t1 = t2
+  | (s1 $ s2)         e (t1 $ t2)         = s1 = t1 andalso s2 = t2
   | _ e _ = false