author | wenzelm |
Wed, 28 Apr 2010 13:32:00 +0200 | |
changeset 36456 | 9fd0f1eacd35 |
parent 36455 | 30f96b4b108b |
child 36457 | 7355af2a7e8a |
--- 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