print functions for typs and terms added

--- a/src/Pure/General/ml_syntax.ML	Sun Jan 07 14:05:44 2007 +0100
+++ b/src/Pure/General/ml_syntax.ML	Sun Jan 07 16:21:22 2007 +0100
@@ -16,6 +16,10 @@
   val print_option: ('a -> string) -> 'a option -> string
   val print_char: string -> string
   val print_string: string -> string
+  val print_class: Term.class -> string
+  val print_sort: Term.sort -> string
+  val print_typ: Term.typ -> string
+  val print_term: Term.term -> string
 end;
 
 structure ML_Syntax: ML_SYNTAX =
@@ -63,4 +67,29 @@
 
 val print_string = quote o translate_string print_char;
 
+val print_class = print_string;
+
+val print_sort = print_list print_class;
+
+fun print_typ (Type sTs) =
+    "Type " ^ print_pair print_string (print_list print_typ) sTs
+  | print_typ (TFree sSort) =
+    "TFree " ^ print_pair print_string print_sort sSort
+  | print_typ (TVar siSort) =
+    "TVar " ^ print_pair (print_pair print_string Int.toString)
+                print_sort siSort;
+
+fun print_term (Const sT) =
+    "Const " ^ print_pair print_string print_typ sT
+  | print_term (Free sT) =
+    "Free " ^ print_pair print_string print_typ sT
+  | print_term (Var siT) =
+    "Var " ^ print_pair (print_pair print_string Int.toString) print_typ siT
+  | print_term (Bound i) =
+    "Bound " ^ Int.toString 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 ^ ")";
+
 end;