diff -r 7b60e4e74430 -r 1c036d6216d3 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri Sep 19 14:24:03 2014 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Sep 18 18:48:04 2014 +0200
@@ -90,14 +90,12 @@
                 then print_case tyvars some_thm vars fxy case_expr
                 else print_app tyvars some_thm vars fxy app
             | NONE => print_case tyvars some_thm vars fxy case_expr)
-    and print_app_expr tyvars some_thm vars ({ sym, dom, range, annotate, ... }, ts) =
+    and print_app_expr tyvars some_thm vars ({ sym, annotation, ... }, ts) =
       let
-        val ty = Library.foldr (op `->) (dom, range)
         val printed_const =
-          if annotate then
-            brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
-          else
-            (str o deresolve) sym
+          case annotation of
+            SOME ty => brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
+          | NONE => (str o deresolve) sym
       in 
         printed_const :: map (print_term tyvars some_thm vars BR) ts
       end
@@ -241,7 +239,7 @@
                   ]
               | SOME (k, Code_Printer.Complex_printer _) =>
                   let
-                    val { sym = Constant c, dom, range, ... } = const;
+                    val { sym = Constant c, dom, ... } = const;
                     val (vs, rhs) = (apfst o map) fst
                       (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
                     val s = if (is_some o const_syntax) c
@@ -249,7 +247,7 @@
                     val vars = reserved
                       |> intro_vars (map_filter I (s :: vs));
                     val lhs = IConst { sym = Constant classparam, typargs = [],
-                      dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
+                      dicts = [], dom = dom, annotation = NONE } `$$ map IVar vs;
                       (*dictionaries are not relevant at this late stage,
                         and these consts never need type annotations for disambiguation *)
                   in