src/Pure/axclass.ML
changeset 36456 9fd0f1eacd35
parent 36430 0a7fdd584391
child 36610 bafd82950e24
     1.1 --- a/src/Pure/axclass.ML	Wed Apr 28 12:23:14 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Wed Apr 28 13:32:00 2010 +0200
     1.3 @@ -190,9 +190,9 @@
     1.4  
     1.5  infix 0 RSO;
     1.6  
     1.7 -fun (SOME a RSO SOME b) = SOME (a RS b)
     1.8 -  | (x RSO NONE) = x
     1.9 -  | (NONE RSO y) = y;
    1.10 +fun (SOME a) RSO (SOME b) = SOME (a RS b)
    1.11 +  | x RSO NONE = x
    1.12 +  | NONE RSO y = y;
    1.13  
    1.14  fun the_classrel thy (c1, c2) =
    1.15    (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of