1.1 --- a/src/Tools/Code/code_haskell.ML	Tue Sep 20 01:32:04 2011 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Sep 20 09:30:19 2011 +0200
     1.3 @@ -85,13 +85,16 @@
     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, body_typ)), annotate)), ts) =
     1.8 +    and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
     1.9        let
    1.10 -        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (function_typs, body_typ)
    1.11 -        fun put_annotation c = brackets [c, str "::", print_typ tyvars NOBR ty]
    1.12 +        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
    1.13 +        val printed_const =
    1.14 +          if annotate then
    1.15 +            brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
    1.16 +          else
    1.17 +            (str o deresolve) c
    1.18        in 
    1.19 -        ((if annotate then put_annotation else I)
    1.20 -          ((str o deresolve) c)) :: map (print_term tyvars some_thm vars BR) ts
    1.21 +        printed_const :: map (print_term tyvars some_thm vars BR) ts
    1.22        end
    1.23      and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
    1.24      and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
    1.25 @@ -234,15 +237,16 @@
    1.26                      ]
    1.27                  | SOME k =>
    1.28                      let
    1.29 -                      val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *)
    1.30 +                      val (c, ((_, tys), _)) = const;
    1.31                        val (vs, rhs) = (apfst o map) fst
    1.32                          (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
    1.33                        val s = if (is_some o const_syntax) c
    1.34                          then NONE else (SOME o Long_Name.base_name o deresolve) c;
    1.35                        val vars = reserved
    1.36                          |> intro_vars (map_filter I (s :: vs));
    1.37 -                      val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs;
    1.38 -                        (*dictionaries are not relevant at this late stage*)
    1.39 +                      val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
    1.40 +                        (*dictionaries are not relevant at this late stage,
    1.41 +                          and these consts never need type annotations for disambiguation *)
    1.42                      in
    1.43                        semicolon [
    1.44                          print_term tyvars (SOME thm) vars NOBR lhs,
    1.45 @@ -323,8 +327,7 @@
    1.46        in deriv [] tyco end;
    1.47      fun print_stmt deresolve = print_haskell_stmt labelled_name
    1.48        class_syntax tyco_syntax const_syntax (make_vars reserved)
    1.49 -      deresolve
    1.50 -      (if string_classes then deriving_show else K false);
    1.51 +      deresolve (if string_classes then deriving_show else K false);
    1.52  
    1.53      (* print modules *)
    1.54      val import_includes_ps =