src/Pure/General/symbol_pos.ML
changeset 54732 b01bb3d09928
parent 53016 fa9c38891cf2
child 55033 8e8243975860
     1.1 --- a/src/Pure/General/symbol_pos.ML	Thu Dec 12 22:38:25 2013 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Dec 12 22:56:28 2013 +0100
     1.3 @@ -220,10 +220,7 @@
     1.4  val letter = Scan.one (symbol #> Symbol.is_letter);
     1.5  val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
     1.6  
     1.7 -val sub =
     1.8 -  Scan.one (symbol #> (fn s =>
     1.9 -    if ! legacy_isub_isup then s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>"
    1.10 -    else s = "\\<^sub>"));
    1.11 +val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>"));
    1.12  
    1.13  in
    1.14