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