tuned;

--- a/src/Pure/sorts.ML	Sun Apr 11 13:08:14 2010 +0200
+++ b/src/Pure/sorts.ML	Sun Apr 11 13:13:23 2010 +0200
@@ -415,11 +415,11 @@
         SOME d1 => class_relation T d1 c2
       | NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
 
-    fun derive _ [] = []
-      | derive (T as Type (a, Us)) S =
+    fun derive (_, []) = []
+      | derive (T as Type (a, Us), S) =
           let
             val Ss = mg_domain algebra a S;
-            val dom = map2 (fn U => fn S => derive U S ~~ S) Us Ss;
+            val dom = map2 (fn U => fn S => derive (U, S) ~~ S) Us Ss;
           in
             S |> map (fn c =>
               let
@@ -427,8 +427,8 @@
                 val dom' = map (fn ((U, d), S') => weaken U d S' ~~ S') ((Us ~~ dom) ~~ Ss');
               in class_relation T (type_constructor (a, Us) dom' c0, c0) c end)
           end
-      | derive T S = weaken T (type_variable T) S;
-  in uncurry derive end;
+      | derive (T, S) = weaken T (type_variable T) S;
+  in derive end;
 
 fun classrel_derivation algebra class_relation =
   let