--- a/src/Tools/Code/code_preproc.ML Mon Aug 09 11:38:32 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Mon Aug 09 13:43:01 2010 +0200
@@ -387,7 +387,7 @@
else let
val lhs = map_index (fn (k, (v, _)) =>
(v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
- val cert = Code.constrain_cert thy (map snd lhs) proto_cert;
+ val cert = Code.constrain_cert thy (map (Sign.minimize_sort thy o snd) lhs) proto_cert;
val (vs, rhss') = Code.typargs_deps_of_cert thy cert;
val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
in (map (pair c) rhss' @ rhss, eqngr') end;