# HG changeset patch
# User wenzelm
# Date 901877633 -7200
# Node ID fdc28193ccf7ae515c32da5c043b3431e19260de
# Parent  7c8abffc4413512b400d222438b9023235056f2d
Pretty.sym;

diff -r 7c8abffc4413 -r fdc28193ccf7 src/Pure/Syntax/ROOT.ML
--- 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";
diff -r 7c8abffc4413 -r fdc28193ccf7 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);