# HG changeset patch
# User wenzelm
# Date 1274101364 -7200
# Node ID cdb9e83abfbecd5c8201dd7eaf281ecf9dbc0160
# Parent  21be4832c36240c1c2e24b294bf4530116b2d083
tuned signature;

diff -r 21be4832c362 -r cdb9e83abfbe src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Mon May 17 14:23:54 2010 +0200
+++ b/src/Pure/General/symbol_pos.ML	Mon May 17 15:02:44 2010 +0200
@@ -4,17 +4,12 @@
 Symbols with explicit position information.
 *)
 
-signature BASIC_SYMBOL_POS =
+signature SYMBOL_POS =
 sig
   type T = Symbol.symbol * Position.T
   val symbol: T -> Symbol.symbol
   val $$$ : Symbol.symbol -> T list -> T list * T list
   val ~$$$ : Symbol.symbol -> T list -> T list * T list
-end
-
-signature SYMBOL_POS =
-sig
-  include BASIC_SYMBOL_POS
   val content: T list -> string
   val untabify_content: T list -> string
   val is_eof: T -> bool
@@ -185,5 +180,10 @@
 
 end;
 
-structure Basic_Symbol_Pos: BASIC_SYMBOL_POS = Symbol_Pos;   (*not open by default*)
+structure Basic_Symbol_Pos =   (*not open by default*)
+struct
+  val symbol = Symbol_Pos.symbol;
+  val $$$ = Symbol_Pos.$$$;
+  val ~$$$ = Symbol_Pos.~$$$;
+end;