# HG changeset patch
# User wenzelm
# Date 1169298558 -3600
# Node ID dd8a81e84a1c78f876ef246dc78e643b913c1a67
# Parent  0f26cd597193514d999296c4b97af8f289629289
tuned;

diff -r 0f26cd597193 -r dd8a81e84a1c src/Pure/General/ml_syntax.ML
--- a/src/Pure/General/ml_syntax.ML	Sat Jan 20 14:09:17 2007 +0100
+++ b/src/Pure/General/ml_syntax.ML	Sat Jan 20 14:09:18 2007 +0100
@@ -45,7 +45,7 @@
   not (is_reserved name) andalso Syntax.is_ascii_identifier name;
 
 
-(* unformatted output *)
+(* literal output -- unformatted *)
 
 fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
 
@@ -71,19 +71,19 @@
 
 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_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_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
+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
   | print_term (Abs (s, T, t)) =