# HG changeset patch
# User wenzelm
# Date 1390069892 -3600
# Node ID 68afbb5ce4ffd675641bcd2d971d9e626f665a6e
# Parent  04b443d54aee3643ccdbcb116a405966fccc4b6c
unused;

diff -r 04b443d54aee -r 68afbb5ce4ff src/Pure/General/symbol_pos.ML
--- 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
diff -r 04b443d54aee -r 68afbb5ce4ff src/Pure/Isar/token.scala
--- 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
diff -r 04b443d54aee -r 68afbb5ce4ff src/Pure/Syntax/lexicon.ML
--- 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),