src/Pure/Syntax/pretty.ML

--- a/src/Pure/Syntax/pretty.ML	Fri Jul 31 11:33:30 1998 +0200
+++ b/src/Pure/Syntax/pretty.ML	Fri Jul 31 11:33:53 1998 +0200
@@ -28,6 +28,7 @@
   type T
   val str: string -> T
   val strlen: string -> int -> T
+  val sym: string -> T
   val brk: int -> T
   val fbrk: T
   val blk: int * T list -> T
@@ -147,6 +148,7 @@
 
 fun str s = String (s, size s);
 fun strlen s len = String (s, len);
+fun sym s = String (s, Symbol.size s);
 
 fun brk wd = Break (false, wd);
 val fbrk = Break (true, 0);