# HG changeset patch
# User haftmann
# Date 1259772816 -3600
# Node ID f31d645b4e0095eea248e6f946b339b5420b9ca4
# Parent  6a03c894fef81cf2a4bb640032090c957a4b579b
subst_signatures

diff -r 6a03c894fef8 -r f31d645b4e00 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Dec 02 17:53:35 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML	Wed Dec 02 17:53:36 2009 +0100
@@ -711,7 +711,7 @@
 and translate_eqn thy algbr eqngr (thm, proper) =
   let
     val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
-      o Logic.unvarify o prop_of) thm;
+      o Code.subst_signatures thy o Logic.unvarify o prop_of) thm;
   in
     fold_map (translate_term thy algbr eqngr (SOME thm)) args
     ##>> translate_term thy algbr eqngr (SOME thm) rhs
@@ -888,7 +888,7 @@
     val stmt_value =
       fold_map (translate_tyvar_sort thy algbr eqngr) vs
       ##>> translate_typ thy algbr eqngr ty
-      ##>> translate_term thy algbr eqngr NONE t
+      ##>> translate_term thy algbr eqngr NONE (Code.subst_signatures thy t)
       #>> (fn ((vs, ty), t) => Fun
         (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
     fun term_value (dep, (naming, program1)) =