more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;

--- a/src/Pure/General/scan.scala	Thu Aug 08 17:24:31 2013 +0200
+++ b/src/Pure/General/scan.scala	Thu Aug 08 17:36:14 2013 +0200
@@ -349,15 +349,13 @@
       : Parser[Token] =
     {
       val letdigs1 = many1(Symbol.is_letdig)
-      val sub_sup =
+      val sub =
         one(s =>
           s == Symbol.sub_decoded || s == "\\<^sub>" ||
-          s == Symbol.isub_decoded || s == "\\<^isub>" ||
-          s == Symbol.sup_decoded || s == "\\<^sup>" ||
-          s == Symbol.isup_decoded || s == "\\<^isup>")
+          s == Symbol.isub_decoded || s == "\\<^isub>")
       val id =
         one(Symbol.is_letter) ~
-          (rep(letdigs1 | (sub_sup ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^
+          (rep(letdigs1 | (sub ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^
         { case x ~ y => x + y }
 
       val nat = many1(Symbol.is_digit)

--- a/src/Pure/General/symbol.ML	Thu Aug 08 17:24:31 2013 +0200
+++ b/src/Pure/General/symbol.ML	Thu Aug 08 17:36:14 2013 +0200
@@ -517,8 +517,6 @@
 
 fun symbolic_end (_ :: "\\<^sub>" :: _) = true
   | symbolic_end (_ :: "\\<^isub>" :: _) = true
-  | symbolic_end (_ :: "\\<^sup>" :: _) = true
-  | symbolic_end (_ :: "\\<^isup>" :: _) = true
   | symbolic_end (s :: _) = is_symbolic s
   | symbolic_end [] = false;
 

--- a/src/Pure/General/symbol_pos.ML	Thu Aug 08 17:24:31 2013 +0200
+++ b/src/Pure/General/symbol_pos.ML	Thu Aug 08 17:36:14 2013 +0200
@@ -217,14 +217,11 @@
 
 val letter = Scan.one (symbol #> Symbol.is_letter);
 val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
-val sub_sup =
-  Scan.one (symbol #>
-    (fn s => s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^sup>" orelse s = "\\<^isup>"));
+val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>" orelse s = "\\<^isub>"));
 
 in
 
-val scan_ident =
-  letter ::: (Scan.repeat (letdigs1 || sub_sup ::: letdigs1) >> flat);
+val scan_ident = letter ::: (Scan.repeat (letdigs1 || sub ::: letdigs1) >> flat);
 
 end;
 

--- a/src/Pure/Syntax/lexicon.ML	Thu Aug 08 17:24:31 2013 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Aug 08 17:36:14 2013 +0200
@@ -296,8 +296,6 @@
     fun chop_idx [] ds = idxname [] ds
       | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
       | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
-      | chop_idx (cs as (_ :: "\\<^sup>" :: _)) ds = idxname cs ds
-      | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
       | chop_idx (c :: cs) ds =
           if Symbol.is_digit c then chop_idx cs (c :: ds)
           else idxname (c :: cs) ds;

--- a/src/Pure/term.ML	Thu Aug 08 17:24:31 2013 +0200
+++ b/src/Pure/term.ML	Thu Aug 08 17:36:14 2013 +0200
@@ -980,8 +980,6 @@
       (case rev (Symbol.explode x) of
         _ :: "\\<^sub>" :: _ => false
       | _ :: "\\<^isub>" :: _ => false
-      | _ :: "\\<^sup>" :: _ => false
-      | _ :: "\\<^isup>" :: _ => false
       | c :: _ => Symbol.is_digit c
       | _ => true);
   in