made SML/NJ happy;
authorwenzelm
Wed, 28 Apr 2010 13:32:00 +0200
changeset 36456 9fd0f1eacd35
parent 36455 30f96b4b108b
child 36457 7355af2a7e8a
made SML/NJ happy;
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