--- a/src/Pure/General/symbol_pos.ML Sat Jan 18 19:24:45 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML Sat Jan 18 19:31:32 2014 +0100
@@ -4,8 +4,6 @@
Symbols with explicit position information.
*)
-val legacy_isub_isup = Unsynchronized.ref false;
-
signature SYMBOL_POS =
sig
type T = Symbol.symbol * Position.T
--- a/src/Pure/Isar/token.scala Sat Jan 18 19:24:45 2014 +0100
+++ b/src/Pure/Isar/token.scala Sat Jan 18 19:31:32 2014 +0100
@@ -71,12 +71,6 @@
def is_command: Boolean = kind == Token.Kind.COMMAND
def is_keyword: Boolean = kind == Token.Kind.KEYWORD
def is_operator: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
- def is_delimited: Boolean =
- kind == Token.Kind.STRING ||
- kind == Token.Kind.ALT_STRING ||
- kind == Token.Kind.VERBATIM ||
- kind == Token.Kind.CARTOUCHE ||
- kind == Token.Kind.COMMENT
def is_ident: Boolean = kind == Token.Kind.IDENT
def is_sym_ident: Boolean = kind == Token.Kind.SYM_IDENT
def is_string: Boolean = kind == Token.Kind.STRING
--- a/src/Pure/Syntax/lexicon.ML Sat Jan 18 19:24:45 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML Sat Jan 18 19:31:32 2014 +0100
@@ -34,11 +34,6 @@
val eof: token
val is_eof: token -> bool
val stopper: token Scan.stopper
- val idT: typ
- val longidT: typ
- val varT: typ
- val tidT: typ
- val tvarT: typ
val terminals: string list
val is_terminal: string -> bool
val literal_markup: string -> Markup.T
@@ -145,12 +140,6 @@
(* terminal arguments *)
-val idT = Type ("id", []);
-val longidT = Type ("longid", []);
-val varT = Type ("var", []);
-val tidT = Type ("tid", []);
-val tvarT = Type ("tvar", []);
-
val terminal_kinds =
[("id", IdentSy),
("longid", LongIdentSy),