src/Pure/axclass.ML
changeset 36456 9fd0f1eacd35
parent 36430 0a7fdd584391
child 36610 bafd82950e24
--- 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