# HG changeset patch
# User wenzelm
# Date 1272454320 -7200
# Node ID 9fd0f1eacd3595393ab5af049a4bcd3646511bb3
# Parent  30f96b4b108b6227a38589b3ebb3506d49172385
made SML/NJ happy;

diff -r 30f96b4b108b -r 9fd0f1eacd35 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Apr 28 12:23:14 2010 +0200
+++ b/src/Pure/axclass.ML	Wed Apr 28 13:32:00 2010 +0200
@@ -190,9 +190,9 @@
 
 infix 0 RSO;
 
-fun (SOME a RSO SOME b) = SOME (a RS b)
-  | (x RSO NONE) = x
-  | (NONE RSO y) = y;
+fun (SOME a) RSO (SOME b) = SOME (a RS b)
+  | x RSO NONE = x
+  | NONE RSO y = y;
 
 fun the_classrel thy (c1, c2) =
   (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of