# HG changeset patch
# User haftmann
# Date 1281354181 -7200
# Node ID 62abd53f37fa11dc592e815c9c61aaa179fcfd56
# Parent  b32a443611868dd652472864b7f0510e3e44b728
minimize sorts in certificate instantiation

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;