src/Tools/Code/code_thingol.ML
changeset 32350 5ef633275b15
parent 32273 3c395fc7ec5e
child 32353 0ac26087464b
     1.1 --- a/src/Tools/Code/code_thingol.ML	Fri Jul 31 10:49:09 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Aug 10 08:37:37 2009 +0200
     1.3 @@ -498,15 +498,15 @@
     1.4      fun stmt_classparam class =
     1.5        ensure_class thy algbr funcgr class
     1.6        #>> (fn class => Classparam (c, class));
     1.7 -    fun stmt_fun ((vs, ty), raw_thms) =
     1.8 +    fun stmt_fun ((vs, ty), raw_eqns) =
     1.9        let
    1.10 -        val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
    1.11 -          then raw_thms
    1.12 -          else (map o apfst) (Code.expand_eta thy 1) raw_thms;
    1.13 +        val eqns = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
    1.14 +          then raw_eqns
    1.15 +          else (map o apfst) (Code.expand_eta thy 1) raw_eqns;
    1.16        in
    1.17          fold_map (translate_tyvar_sort thy algbr funcgr) vs
    1.18          ##>> translate_typ thy algbr funcgr ty
    1.19 -        ##>> fold_map (translate_eq thy algbr funcgr) thms
    1.20 +        ##>> translate_eqns thy algbr funcgr eqns
    1.21          #>> (fn info => Fun (c, info))
    1.22        end;
    1.23      val stmt_const = case Code.get_datatype_of_constr thy c
    1.24 @@ -597,7 +597,10 @@
    1.25              translate_term thy algbr funcgr thm t'
    1.26              ##>> fold_map (translate_term thy algbr funcgr thm) ts
    1.27              #>> (fn (t, ts) => t `$$ ts)
    1.28 -and translate_eq thy algbr funcgr (thm, proper) =
    1.29 +and translate_eqns thy algbr funcgr eqns =
    1.30 +  fold_map (translate_eqn thy algbr funcgr)
    1.31 +    (burrow_fst (Code.desymbolize_all_vars thy) eqns)
    1.32 +and translate_eqn thy algbr funcgr (thm, proper) =
    1.33    let
    1.34      val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
    1.35        o Logic.unvarify o prop_of) thm;