made SML/NJ happy;
authorwenzelm
Wed Apr 28 13:32:00 2010 +0200 (2010-04-28 ago)
changeset 364569fd0f1eacd35
parent 36455 30f96b4b108b
child 36457 7355af2a7e8a
made SML/NJ happy;
src/Pure/axclass.ML
     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