diff -r 7a9aa69f9b38 -r 85ebb645b1a3 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Mar 08 21:07:46 2016 +0100
+++ b/src/Tools/Code/code_thingol.ML	Tue Mar 08 21:07:47 2016 +0100
@@ -482,7 +482,7 @@
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
     val typarg_witnesses = Sorts.of_sort_derivation algebra
-      {class_relation = K (Sorts.classrel_derivation algebra class_relation),
+      {class_relation = fn _ => fn _ => 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 ctxt permissive some_thm deps ty sort e;