src/Tools/Code/code_haskell.ML

            of SOME (app as ({ sym = Constant const, ... }, _)) =>
                 if is_none (const_syntax const)
                 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
     and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
     and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p

                     str "=",
                     print_app tyvars (SOME thm) reserved NOBR (const, [])
                   ]
               | 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
                       then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
                     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
                     semicolon [
                       print_term tyvars (SOME thm) vars NOBR lhs,