Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Incompatibility with SML/NJ fixed.
authorballarin
Fri, 29 Nov 2002 14:26:55 +0100
changeset 13738 d48d1716bb6d
parent 13737 e564c3d2d174
child 13739 f5d0a66c8124
Incompatibility with SML/NJ fixed.
src/HOL/Algebra/abstract/order.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle