src/Tools/code/code_haskell.ML

       (map (uncurry pr_module) includes
         @ map serialize_module (Symtab.dest hs_program))
       destination
   end;
 
+val literals = let
+  fun char_haskell c =
+    let
+      val s = ML_Syntax.print_char c;
+    in if s = "'" then "\\'" else s end;
+in Literals {
+  literal_char = enclose "'" "'" o char_haskell,
+  literal_string = quote o translate_string char_haskell,
+  literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
+    else enclose "(" ")" (signed_string_of_int k),
+  literal_list = Pretty.enum "," "[" "]",
+  infix_cons = (5, ":")
+} end;
+
 
 (** optional monad syntax **)
 
 fun implode_monad c_bind t =
   let

     >> (fn ((raw_run, raw_bind), target) => Toplevel.theory 
           (add_monad target raw_run raw_bind))
   );
 
 val setup =
-  Code_Target.add_target (target, isar_seri_haskell)
+  Code_Target.add_target (target, (isar_seri_haskell, literals))
   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy [
         pr_typ (INFX (1, X)) ty1,
         str "->",
         pr_typ (INFX (1, R)) ty2