src/Pure/General/symbol_pos.ML
changeset 30576 49899f26fbd1
parent 29606 fedb8be05f24
child 30589 9674f64a0702
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Mar 18 20:03:01 2009 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Mar 18 21:55:38 2009 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4    val explode: text * Position.T -> T list
     1.5  end;
     1.6  
     1.7 -structure SymbolPos: SYMBOL_POS =
     1.8 +structure Symbol_Pos: SYMBOL_POS =
     1.9  struct
    1.10  
    1.11  (* type T *)
    1.12 @@ -149,5 +149,5 @@
    1.13  
    1.14  end;
    1.15  
    1.16 -structure BasicSymbolPos: BASIC_SYMBOL_POS = SymbolPos;   (*not open by default*)
    1.17 +structure Basic_Symbol_Pos: BASIC_SYMBOL_POS = Symbol_Pos;   (*not open by default*)
    1.18