# HG changeset patch
# User wenzelm
# Date 1168255573 -3600
# Node ID 91f1731b57c2ec8410c6fd68f27b05ceadc0ccb4
# Parent  3a3f16fccb83549aad087f06efdc32459b9edfa9
tuned signature;

diff -r 3a3f16fccb83 -r 91f1731b57c2 src/Pure/General/ml_syntax.ML
--- a/src/Pure/General/ml_syntax.ML	Sun Jan 07 16:21:22 2007 +0100
+++ b/src/Pure/General/ml_syntax.ML	Mon Jan 08 12:26:13 2007 +0100
@@ -16,10 +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
+  val print_class: class -> string
+  val print_sort: sort -> string
+  val print_typ: typ -> string
+  val print_term: term -> string
 end;
 
 structure ML_Syntax: ML_SYNTAX =
@@ -72,24 +72,23 @@
 val print_sort = print_list print_class;
 
 fun print_typ (Type sTs) =
-    "Type " ^ print_pair print_string (print_list print_typ) sTs
+      "Type " ^ print_pair print_string (print_list print_typ) sTs
   | print_typ (TFree sSort) =
-    "TFree " ^ print_pair print_string print_sort 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;
+      "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
+      "Const " ^ print_pair print_string print_typ sT
   | print_term (Free sT) =
-    "Free " ^ print_pair print_string print_typ 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
+      "Var " ^ print_pair (print_pair print_string Int.toString) print_typ siT
   | print_term (Bound i) =
-    "Bound " ^ Int.toString i
+      "Bound " ^ Int.toString i
   | print_term (Abs (s, T, t)) =
-    "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
+      "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
   | print_term (t1 $ t2) =
-    "(" ^ print_term t1 ^ ") $ (" ^ print_term t2 ^ ")";
+      "(" ^ print_term t1 ^ ") $ (" ^ print_term t2 ^ ")";
 
 end;