# HG changeset patch
# User wenzelm
# Date 1354115237 -3600
# Node ID 41fd9f68614b2fb54fc118c8291aa5de3744e89a
# Parent  4aa34bd43228519583bb834341a84142a660c17d
clarified new identifier syntax: exclude \<^isup>, include subscripted prime (to allow imitating full identifier here);

diff -r 4aa34bd43228 -r 41fd9f68614b src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Wed Nov 28 15:59:18 2012 +0100
+++ b/src/Pure/General/symbol_pos.ML	Wed Nov 28 16:07:17 2012 +0100
@@ -220,7 +220,7 @@
 val digit = Symbol.is_ascii_digit;
 fun underscore s = s = "_";
 fun prime s = s = "'";
-fun script s = s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>";
+fun script s = s = "\\<^sub>" orelse s = "\\<^isub>";
 fun special_letter s = Symbol.is_letter_symbol s andalso not (script s);
 
 val scan_plain = Scan.one ((latin orf digit orf prime) o symbol) >> single;
@@ -228,7 +228,7 @@
 val scan_prime = Scan.one (prime o symbol) >> single;
 
 val scan_script =
-  Scan.one (script o symbol) -- Scan.one ((latin orf digit orf special_letter) o symbol)
+  Scan.one (script o symbol) -- Scan.one ((latin orf digit orf prime orf special_letter) o symbol)
   >> (fn (x, y) => [x, y]);
 
 val scan_ident_part1 =