# HG changeset patch
# User wenzelm
# Date 1270984403 -7200
# Node ID b2b9b687a4c411e5a72c9478cb6e8639d70ce12d
# Parent  a51d1d154c710c8d8e50d6396b0d7c1f0bfd0456
tuned;

diff -r a51d1d154c71 -r b2b9b687a4c4 src/Pure/sorts.ML
--- 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