Pretty.sym;

--- a/src/Pure/Syntax/ROOT.ML	Fri Jul 31 11:33:30 1998 +0200
+++ b/src/Pure/Syntax/ROOT.ML	Fri Jul 31 11:33:53 1998 +0200
@@ -6,10 +6,10 @@
 *)
 
 (*generic modules*)
-use "pretty.ML";
 use "scan.ML";
 use "source.ML";
 use "symbol.ML";
+use "pretty.ML";
 
 (*actual syntax module*)
 use "lexicon.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);