# HG changeset patch
# User wenzelm
# Date 857144738 -3600
# Node ID 932fae4271d78bda8778c408605b7619b15ba8a7
# Parent  8bccb3ab4ca40d533e310881b0a7dfa456f7eba7
term_of_... now mark class, tfree, tvar;

diff -r 8bccb3ab4ca4 -r 932fae4271d7 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Fri Feb 28 16:44:30 1997 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Fri Feb 28 16:45:38 1997 +0100
@@ -94,11 +94,11 @@
 
 (** output utils **)
 
-(* term_of_sort *)		(* FIXME mark whole sort vs. ind. classes !? *)
+(* term_of_sort *)
 
 fun term_of_sort S =
   let
-    fun class c = free c;       (* FIXME mark *)
+    fun class c = const "_class" $ free c;
 
     fun classes [] = sys_error "term_of_sort"
       | classes [c] = class c
@@ -119,9 +119,9 @@
       if show_sorts then const "_ofsort" $ t $ term_of_sort S
       else t;
 
-    fun term_of (Type (a, tys)) = list_comb (const a, map term_of tys)
-      | term_of (TFree (x, S)) = of_sort (free x) S	(* FIXME mark? *)
-      | term_of (TVar (xi, S)) = of_sort (var xi) S;	(* FIXME mark? *)
+    fun term_of (Type (a, Ts)) = list_comb (const a, map term_of Ts)
+      | term_of (TFree (x, S)) = of_sort (const "_tfree" $ free x) S
+      | term_of (TVar (xi, S)) = of_sort (const "_tvar" $ var xi) S;
   in
     term_of ty
   end;
@@ -188,6 +188,7 @@
    [],
    [],
    [("fun", fun_ast_tr')])
+  TokenTrans.token_translation
   ([], []);
 
 end;