src/Pure/term.ML
changeset 54732 b01bb3d09928
parent 53016 fa9c38891cf2
child 56241 029246729dc0
     1.1 --- a/src/Pure/term.ML	Thu Dec 12 22:38:25 2013 +0100
     1.2 +++ b/src/Pure/term.ML	Thu Dec 12 22:56:28 2013 +0100
     1.3 @@ -979,8 +979,6 @@
     1.4      val dot =
     1.5        (case rev (Symbol.explode x) of
     1.6          _ :: "\\<^sub>" :: _ => false
     1.7 -      | _ :: "\\<^isub>" :: _ => false  (*legacy*)
     1.8 -      | _ :: "\\<^isup>" :: _ => false  (*legacy*)
     1.9        | c :: _ => Symbol.is_digit c
    1.10        | _ => true);
    1.11    in