disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;

--- a/NEWS	Tue Aug 13 16:25:47 2013 +0200
+++ b/NEWS	Tue Aug 13 17:26:22 2013 +0200
@@ -6,6 +6,17 @@
 
 *** General ***
 
+* Simplified subscripts within identifiers, using plain \<^sub>
+instead of the second copy \<^isub> and \<^isup>.  Superscripts are
+only for literal tokens within notation; explicit mixfix annotations
+for consts or fixed variables may be used as fall-back for unusual
+names.  Obsolete \<twosuperior> has been expanded to \<^sup>2 in
+Isabelle/HOL.  INCOMPATIBILITY, use "isabelle update_sub_sup" to
+standardize symbols as a starting point for further manual cleanup.
+The ML reference variable "legacy_isub_isup" may be set as temporary
+workaround, to make the prover accept a subset of the old identifier
+syntax.
+
 * Uniform management of "quick_and_dirty" as system option (see also
 "isabelle options"), configuration option within the context (see also
 Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor

--- a/src/Pure/General/symbol.ML	Tue Aug 13 16:25:47 2013 +0200
+++ b/src/Pure/General/symbol.ML	Tue Aug 13 17:26:22 2013 +0200
@@ -516,7 +516,8 @@
 (* bump string -- treat as base 26 or base 1 numbers *)
 
 fun symbolic_end (_ :: "\\<^sub>" :: _) = true
-  | symbolic_end (_ :: "\\<^isub>" :: _) = true
+  | symbolic_end (_ :: "\\<^isub>" :: _) = true  (*legacy*)
+  | symbolic_end (_ :: "\\<^isup>" :: _) = true  (*legacy*)
   | symbolic_end (s :: _) = is_symbolic s
   | symbolic_end [] = false;
 

--- a/src/Pure/General/symbol_pos.ML	Tue Aug 13 16:25:47 2013 +0200
+++ b/src/Pure/General/symbol_pos.ML	Tue Aug 13 17:26:22 2013 +0200
@@ -4,6 +4,8 @@
 Symbols with explicit position information.
 *)
 
+val legacy_isub_isup = Unsynchronized.ref false;
+
 signature SYMBOL_POS =
 sig
   type T = Symbol.symbol * Position.T
@@ -217,7 +219,11 @@
 
 val letter = Scan.one (symbol #> Symbol.is_letter);
 val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
-val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>" orelse s = "\\<^isub>"));
+
+val sub =
+  Scan.one (symbol #> (fn s =>
+    if ! legacy_isub_isup then s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>"
+    else s = "\\<^sub>"));
 
 in
 

--- a/src/Pure/Syntax/lexicon.ML	Tue Aug 13 16:25:47 2013 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Aug 13 17:26:22 2013 +0200
@@ -295,7 +295,8 @@
     fun idxname cs ds = (implode (rev cs), nat 0 ds);
     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 (_ :: "\\<^isub>" :: _)) ds = idxname cs ds  (*legacy*)
+      | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds  (*legacy*)
       | 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	Tue Aug 13 16:25:47 2013 +0200
+++ b/src/Pure/term.ML	Tue Aug 13 17:26:22 2013 +0200
@@ -979,7 +979,8 @@
     val dot =
       (case rev (Symbol.explode x) of
         _ :: "\\<^sub>" :: _ => false
-      | _ :: "\\<^isub>" :: _ => false
+      | _ :: "\\<^isub>" :: _ => false  (*legacy*)
+      | _ :: "\\<^isup>" :: _ => false  (*legacy*)
       | c :: _ => Symbol.is_digit c
       | _ => true);
   in