diff -r b32a44361186 -r 62abd53f37fa src/Tools/Code/code_preproc.ML --- 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;