--- 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;