# HG changeset patch
# User wenzelm
# Date 1153303928 -7200
# Node ID 4de20306a88ae4842cef0c2521624648d5b713a3
# Parent  928c8dc07216ba0dfbdb6b0bf40f3dfb8154212e
export is_tid;

diff -r 928c8dc07216 -r 4de20306a88a src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Jul 19 12:12:07 2006 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Wed Jul 19 12:12:08 2006 +0200
@@ -9,6 +9,7 @@
 sig
   val is_identifier: string -> bool
   val is_ascii_identifier: string -> bool
+  val is_tid: string -> bool
   val implode_xstr: string list -> string
   val explode_xstr: string -> string list
   val scan_id: string list -> string * string list
@@ -39,7 +40,6 @@
 sig
   include LEXICON0
   val is_xid: string -> bool
-  val is_tid: string -> bool
   datatype token =
     Token of string |
     IdentSy of string |