src/Pure/General/symbol_pos.ML
changeset 40525 14a2e686bdac
parent 36957 cdb9e83abfbe
child 41416 a2208d3e2bd6
     1.1 --- a/src/Pure/General/symbol_pos.ML	Sat Nov 13 19:27:41 2010 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Sat Nov 13 19:47:23 2010 +0100
     1.3 @@ -182,7 +182,6 @@
     1.4  
     1.5  structure Basic_Symbol_Pos =   (*not open by default*)
     1.6  struct
     1.7 -  val symbol = Symbol_Pos.symbol;
     1.8    val $$$ = Symbol_Pos.$$$;
     1.9    val ~$$$ = Symbol_Pos.~$$$;
    1.10  end;