src/Tools/Code/code_thingol.ML
changeset 33943 f31d645b4e00
parent 33420 17b7095ad463
child 33972 daf65be6bfe5
     1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Dec 02 17:53:35 2009 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Dec 02 17:53:36 2009 +0100
     1.3 @@ -711,7 +711,7 @@
     1.4  and translate_eqn thy algbr eqngr (thm, proper) =
     1.5    let
     1.6      val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
     1.7 -      o Logic.unvarify o prop_of) thm;
     1.8 +      o Code.subst_signatures thy o Logic.unvarify o prop_of) thm;
     1.9    in
    1.10      fold_map (translate_term thy algbr eqngr (SOME thm)) args
    1.11      ##>> translate_term thy algbr eqngr (SOME thm) rhs
    1.12 @@ -888,7 +888,7 @@
    1.13      val stmt_value =
    1.14        fold_map (translate_tyvar_sort thy algbr eqngr) vs
    1.15        ##>> translate_typ thy algbr eqngr ty
    1.16 -      ##>> translate_term thy algbr eqngr NONE t
    1.17 +      ##>> translate_term thy algbr eqngr NONE (Code.subst_signatures thy t)
    1.18        #>> (fn ((vs, ty), t) => Fun
    1.19          (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
    1.20      fun term_value (dep, (naming, program1)) =