# HG changeset patch # User wenzelm # Date 1272454320 -7200 # Node ID 9fd0f1eacd3595393ab5af049a4bcd3646511bb3 # Parent 30f96b4b108b6227a38589b3ebb3506d49172385 made SML/NJ happy; diff -r 30f96b4b108b -r 9fd0f1eacd35 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