# HG changeset patch
# User wenzelm
# Date 1169402977 -3600
# Node ID 3888f1dd45d5176f438c35e485362595ea8337c4
# Parent  649e1d769e15418df8c60f9a1e8f46288ae3e0df
added atomic, print_int;
tuned;

diff -r 649e1d769e15 -r 3888f1dd45d5 src/Pure/General/ml_syntax.ML
--- a/src/Pure/General/ml_syntax.ML	Sun Jan 21 19:09:36 2007 +0100
+++ b/src/Pure/General/ml_syntax.ML	Sun Jan 21 19:09:37 2007 +0100
@@ -11,6 +11,8 @@
   val reserved: Name.context
   val is_reserved: string -> bool
   val is_identifier: string -> bool
+  val atomic: string -> string
+  val print_int: int -> string
   val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
   val print_list: ('a -> string) -> 'a list -> string
   val print_option: ('a -> string) -> 'a option -> string
@@ -47,6 +49,10 @@
 
 (* literal output -- unformatted *)
 
+val atomic = enclose "(" ")";
+
+val print_int = Int.toString;
+
 fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
 
 fun print_list f = enclose "[" "]" o commas o map f;
@@ -71,24 +77,16 @@
 
 val print_sort = print_list print_class;
 
-fun print_typ (Type arg) =
-      "Type " ^ print_pair print_string (print_list print_typ) arg
-  | print_typ (TFree arg) =
-      "TFree " ^ print_pair print_string print_sort arg
-  | print_typ (TVar arg) =
-      "TVar " ^ print_pair (print_pair print_string Int.toString) print_sort arg;
+fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg
+  | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg
+  | print_typ (TVar arg) = "TVar " ^ print_pair (print_pair print_string print_int) print_sort arg;
 
-fun print_term (Const arg) =
-      "Const " ^ print_pair print_string print_typ arg
-  | print_term (Free arg) =
-      "Free " ^ print_pair print_string print_typ arg
-  | print_term (Var arg) =
-      "Var " ^ print_pair (print_pair print_string Int.toString) print_typ arg
-  | print_term (Bound i) =
-      "Bound " ^ Int.toString i
+fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg
+  | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg
+  | print_term (Var arg) = "Var " ^ print_pair (print_pair print_string print_int) print_typ arg
+  | print_term (Bound i) = "Bound " ^ print_int i
   | print_term (Abs (s, T, t)) =
       "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
-  | print_term (t1 $ t2) =
-      "(" ^ print_term t1 ^ ") $ (" ^ print_term t2 ^ ")";
+  | print_term (t1 $ t2) = "(" ^ print_term t1 ^ ") $ (" ^ print_term t2 ^ ")";
 
 end;