of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;

--- a/src/Pure/sorts.ML	Fri Apr 09 13:35:54 2010 +0200
+++ b/src/Pure/sorts.ML	Sun Apr 11 13:08:14 2010 +0200
@@ -57,8 +57,8 @@
   val meet_sort_typ: algebra -> typ * sort -> typ -> typ   (*exception CLASS_ERROR*)
   val of_sort: algebra -> typ * sort -> bool
   val of_sort_derivation: algebra ->
-    {class_relation: 'a * class -> class -> 'a,
-     type_constructor: string -> ('a * class) list list -> class -> 'a,
+    {class_relation: typ -> 'a * class -> class -> 'a,
+     type_constructor: string * typ list -> ('a * class) list list -> class -> 'a,
      type_variable: typ -> ('a * class) list} ->
     typ * sort -> 'a list   (*exception CLASS_ERROR*)
   val classrel_derivation: algebra ->
@@ -410,24 +410,24 @@
   let
     val arities = arities_of algebra;
 
-    fun weaken S1 S2 = S2 |> map (fn c2 =>
+    fun weaken T S1 S2 = S2 |> map (fn c2 =>
       (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
-        SOME d1 => class_relation d1 c2
+        SOME d1 => class_relation T d1 c2
       | NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
 
     fun derive _ [] = []
-      | derive (Type (a, Ts)) S =
+      | derive (T as Type (a, Us)) S =
           let
             val Ss = mg_domain algebra a S;
-            val dom = map2 (fn T => fn S => derive T S ~~ S) Ts Ss;
+            val dom = map2 (fn U => fn S => derive U S ~~ S) Us Ss;
           in
             S |> map (fn c =>
               let
                 val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
-                val dom' = map2 (fn d => fn S' => weaken d S' ~~ S') dom Ss';
-              in class_relation (type_constructor a dom' c0, c0) c end)
+                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 (type_variable T) S;
+      | derive T S = weaken T (type_variable T) S;
   in uncurry derive end;
 
 fun classrel_derivation algebra class_relation =

--- a/src/Tools/Code/code_preproc.ML	Fri Apr 09 13:35:54 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Sun Apr 11 13:08:14 2010 +0200
@@ -365,13 +365,13 @@
 fun dicts_of thy (proj_sort, algebra) (T, sort) =
   let
     fun class_relation (x, _) _ = x;
-    fun type_constructor tyco xs class =
+    fun type_constructor (tyco, _) xs class =
       inst_params thy tyco (Sorts.complete_sort algebra [class])
         @ (maps o maps) fst xs;
     fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
   in
     flat (Sorts.of_sort_derivation algebra
-      { class_relation = class_relation, type_constructor = type_constructor,
+      { class_relation = K class_relation, type_constructor = type_constructor,
         type_variable = type_variable } (T, proj_sort sort)
        handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
   end;

--- a/src/Tools/Code/code_thingol.ML	Fri Apr 09 13:35:54 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Sun Apr 11 13:08:14 2010 +0200
@@ -767,14 +767,14 @@
           Global ((class, tyco), yss)
       | class_relation (Local (classrels, v), subclass) superclass =
           Local ((subclass, superclass) :: classrels, v);
-    fun type_constructor tyco yss class =
+    fun type_constructor (tyco, _) yss class =
       Global ((class, tyco), (map o map) fst yss);
     fun type_variable (TFree (v, sort)) =
       let
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
     val typargs = Sorts.of_sort_derivation algebra
-      {class_relation = Sorts.classrel_derivation algebra class_relation,
+      {class_relation = K (Sorts.classrel_derivation algebra class_relation),
        type_constructor = type_constructor,
        type_variable = type_variable} (ty, proj_sort sort)
       handle Sorts.CLASS_ERROR e => not_wellsorted thy some_thm ty sort e;