src/Pure/General/symbol.ML
changeset 14173 a3690aeb79d4
parent 14171 0cab06e3bbd0
child 14221 9276f30eaed6
--- a/src/Pure/General/symbol.ML	Thu Aug 28 02:00:16 2003 +0200
+++ b/src/Pure/General/symbol.ML	Fri Aug 29 13:18:45 2003 +0200
@@ -87,9 +87,6 @@
 
 local
     fun wrap s = "\\<" ^ s ^ ">"
-    val pre_digits =
-	["zero","one","two","three","four",
-	 "five","six","seven","eight","nine"]
 
     val cal_letters =
 	["A","B","C","D","E","F","G","H","I","J","K","L","M",
@@ -119,12 +116,9 @@
 	goth_letters  @
 	greek_letters
 in
-val ext_digits  = map wrap pre_digits
 val ext_letters = map wrap pre_letters
-val ext_letdigs = ext_digits @ ext_letters
-fun is_ext_digit  s = String.isPrefix "\\<" s andalso s mem ext_digits
+
 fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters
-fun is_ext_letdig s = String.isPrefix "\\<" s andalso s mem ext_letdigs
 end
      
 fun is_letter s =
@@ -134,8 +128,7 @@
     orelse is_ext_letter s
 
 fun is_digit s =
-    (size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9")
-    orelse is_ext_digit s
+    size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"
 
 fun is_quasi "_" = true
   | is_quasi "'" = true
@@ -152,11 +145,11 @@
 
 fun is_symbolic s =
   size s > 2 andalso nth_elem_string (2, s) <> "^"
-  andalso not (is_ext_letdig s);
+  andalso not (is_ext_letter s);
 
 fun is_printable s =
   size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
-  is_ext_letdig s orelse
+  is_ext_letter s orelse
   is_symbolic s;
 
 fun is_identifier s =