# HG changeset patch
# User wenzelm
# Date 1386885388 -3600
# Node ID b01bb3d09928d7a638230ac21e5dc99075b78010
# Parent  384ac33802b0f44309c12fd6e4240686bd0feaa6
discontinued legacy_isub_isup;

diff -r 384ac33802b0 -r b01bb3d09928 NEWS
--- a/NEWS	Thu Dec 12 22:38:25 2013 +0100
+++ b/NEWS	Thu Dec 12 22:56:28 2013 +0100
@@ -12,6 +12,10 @@
 * Document antiquotation @{file_unchecked} is like @{file}, but does
 not check existence within the file-system.
 
+* Discontinued legacy_isub_isup, which was a temporary Isabelle/ML
+workaround in Isabelle2013-1.  The prover process no longer accepts
+old identifier syntax with \<^isub> or \<^isup>.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r 384ac33802b0 -r b01bb3d09928 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Dec 12 22:38:25 2013 +0100
+++ b/src/Pure/General/symbol.ML	Thu Dec 12 22:56:28 2013 +0100
@@ -517,8 +517,6 @@
 (* bump string -- treat as base 26 or base 1 numbers *)
 
 fun symbolic_end (_ :: "\\<^sub>" :: _) = true
-  | symbolic_end (_ :: "\\<^isub>" :: _) = true  (*legacy*)
-  | symbolic_end (_ :: "\\<^isup>" :: _) = true  (*legacy*)
   | symbolic_end ("'" :: ss) = symbolic_end ss
   | symbolic_end (s :: _) = is_symbolic s
   | symbolic_end [] = false;
diff -r 384ac33802b0 -r b01bb3d09928 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Thu Dec 12 22:38:25 2013 +0100
+++ b/src/Pure/General/symbol_pos.ML	Thu Dec 12 22:56:28 2013 +0100
@@ -220,10 +220,7 @@
 val letter = Scan.one (symbol #> Symbol.is_letter);
 val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
 
-val sub =
-  Scan.one (symbol #> (fn s =>
-    if ! legacy_isub_isup then s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>"
-    else s = "\\<^sub>"));
+val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>"));
 
 in
 
diff -r 384ac33802b0 -r b01bb3d09928 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Dec 12 22:38:25 2013 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Thu Dec 12 22:56:28 2013 +0100
@@ -295,8 +295,6 @@
     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  (*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;
diff -r 384ac33802b0 -r b01bb3d09928 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Dec 12 22:38:25 2013 +0100
+++ b/src/Pure/term.ML	Thu Dec 12 22:56:28 2013 +0100
@@ -979,8 +979,6 @@
     val dot =
       (case rev (Symbol.explode x) of
         _ :: "\\<^sub>" :: _ => false
-      | _ :: "\\<^isub>" :: _ => false  (*legacy*)
-      | _ :: "\\<^isup>" :: _ => false  (*legacy*)
       | c :: _ => Symbol.is_digit c
       | _ => true);
   in