src/Tools/Code/code_thingol.ML
changeset 33972 daf65be6bfe5
parent 33943 f31d645b4e00
parent 33969 1e7ca47c6c3d
child 33994 fc8af744f63c
     1.1 --- a/src/Tools/Code/code_thingol.ML	Fri Dec 04 12:17:43 2009 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Dec 04 12:22:09 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)) =