src/Tools/Code/code_haskell.ML
changeset 34178 a78b8d5b91cb
parent 34085 420234017d39
child 34269 b5c99df2e4b1
--- a/src/Tools/Code/code_haskell.ML	Wed Dec 23 10:09:06 2009 +0100
+++ b/src/Tools/Code/code_haskell.ML	Wed Dec 23 11:32:08 2009 +0100
@@ -32,7 +32,7 @@
       | SOME class => class;
     fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
      of [] => []
-      | classbinds => Pretty.list "(" ")" (
+      | classbinds => enum "," "(" ")" (
           map (fn (v, class) =>
             str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds)
           @@ str " => ";
@@ -412,11 +412,11 @@
       val s = ML_Syntax.print_char c;
     in if s = "'" then "\\'" else s end;
 in Literals {
-  literal_char = enclose "'" "'" o char_haskell,
+  literal_char = Library.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 "," "[" "]",
+    else Library.enclose "(" ")" (signed_string_of_int k),
+  literal_list = enum "," "[" "]",
   infix_cons = (5, ":")
 } end;
 
@@ -451,7 +451,7 @@
           val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
             (bind :: binds) vars;
         in
-          (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks)
+          (brackify fxy o single o enclose "do {" "}" o Pretty.breaks)
             (ps @| print_term vars' NOBR t'')
         end
       | NONE => brackify_infix (1, L) fxy