1.1 --- a/src/Tools/Code/code_haskell.ML	Wed Sep 07 13:51:34 2011 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Wed Sep 07 13:51:35 2011 +0200
     1.3 @@ -75,20 +75,14 @@
     1.4                  then print_case tyvars some_thm vars fxy cases
     1.5                  else print_app tyvars some_thm vars fxy c_ts
     1.6              | NONE => print_case tyvars some_thm vars fxy cases)
     1.7 -    and print_app_expr tyvars some_thm vars ((c, ((_, (function_typs, _)), _)), ts) = case contr_classparam_typs c
     1.8 -     of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
     1.9 -      | fingerprint => let
    1.10 -          val ts_fingerprint = ts ~~ take (length ts) fingerprint;
    1.11 -          val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
    1.12 -            (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
    1.13 -          fun print_term_anno (t, NONE) _ = print_term tyvars some_thm vars BR t
    1.14 -            | print_term_anno (t, SOME _) ty =
    1.15 -                brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
    1.16 -        in
    1.17 -          if needs_annotation then
    1.18 -            (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
    1.19 -          else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
    1.20 -        end
    1.21 +    and print_app_expr tyvars some_thm vars ((c, ((_, (function_typs, body_typ)), annotate)), ts) =
    1.22 +      let
    1.23 +        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (function_typs, body_typ)
    1.24 +        fun put_annotation c = brackets [c, str "::", print_typ tyvars NOBR ty]
    1.25 +      in 
    1.26 +        ((if annotate then put_annotation else I)
    1.27 +          ((str o deresolve) c)) :: map (print_term tyvars some_thm vars BR) ts
    1.28 +      end
    1.29      and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
    1.30      and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
    1.31      and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =

     2.1 --- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:34 2011 +0200
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:35 2011 +0200
     2.3 @@ -786,16 +786,17 @@
     2.4          then translation_error thy permissive some_thm
     2.5            "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
     2.6        else ()
     2.7 -    val arg_typs = Sign.const_typargs thy (c, ty);
     2.8 +    val (annotate, ty') = (case ty of Type("", [ty']) => (true, ty') | ty' => (false, ty'))
     2.9 +    val arg_typs = Sign.const_typargs thy (c, ty');
    2.10      val sorts = Code_Preproc.sortargs eqngr c;
    2.11 -    val (function_typs, body_typ) = Term.strip_type ty;
    2.12 +    val (function_typs, body_typ) = Term.strip_type ty';
    2.13    in
    2.14      ensure_const thy algbr eqngr permissive c
    2.15      ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
    2.16      ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
    2.17      ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
    2.18      #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
    2.19 -      IConst (c, (((arg_typs, dss), (function_typs, body_typ)), false))) (* FIXME *)
    2.20 +      IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
    2.21    end
    2.22  and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
    2.23    translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)