--- 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 ***
--- 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;
--- 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
--- 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;
--- 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