src/Tools/Code/code_thingol.ML
changeset 32872 019201eb7e07
parent 32795 a0f38d8d633a
child 32873 333945c9ac6a
     1.1 --- a/src/Tools/Code/code_thingol.ML	Sun Oct 04 12:59:22 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Oct 05 08:36:33 2009 +0200
     1.3 @@ -554,16 +554,21 @@
     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), eqns) =
     1.8 -      fold_map (translate_tyvar_sort thy algbr funcgr) vs
     1.9 -      ##>> translate_typ thy algbr funcgr ty
    1.10 -      ##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy) eqns)
    1.11 -      #>> (fn info => Fun (c, info));
    1.12 +    fun stmt_fun raw_eqns =
    1.13 +      let
    1.14 +        val eqns = burrow_fst (clean_thms thy) raw_eqns;
    1.15 +        val ((vs, ty), _) = Code.typscheme_rhss_eqns thy c (map fst 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_eqn thy algbr funcgr) eqns
    1.20 +        #>> (fn info => Fun (c, info))
    1.21 +      end;
    1.22      val stmt_const = case Code.get_datatype_of_constr thy c
    1.23       of SOME tyco => stmt_datatypecons tyco
    1.24        | NONE => (case AxClass.class_of_param thy c
    1.25           of SOME class => stmt_classparam class
    1.26 -          | NONE => stmt_fun (Code_Preproc.typ funcgr c, Code_Preproc.eqns funcgr c))
    1.27 +          | NONE => stmt_fun (Code_Preproc.eqns funcgr c))
    1.28    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
    1.29  and ensure_class thy (algbr as (_, algebra)) funcgr class =
    1.30    let