# HG changeset patch
# User skalberg
# Date 1062155925 -7200
# Node ID a3690aeb79d4e821f6b3cb04ed7a4167df06e347
# Parent  a872d646bf01290f8ece6420bc734fc2d7df1766
Removed the extended digits again.

diff -r a872d646bf01 -r a3690aeb79d4 NEWS
--- a/NEWS	Thu Aug 28 02:00:16 2003 +0200
+++ b/NEWS	Fri Aug 29 13:18:45 2003 +0200
@@ -7,16 +7,15 @@
 *** General ***
 
 * Pure: Greek letters (except small lambda, \<lambda>), as well as gothic
-  (\<aa>,...\<zz>,\<AA>,...,\<ZZ>), caligraphic (\<A>...\<Z>), and
-  euler (\<a>...\<z>), are now considered normal letters, and can
-  therefore be used anywhere where an ASCII letter (a...zA...Z) has
-  until now.  Similarily, the symbol digits \<zero>...\<nine> are now
-  considered normal digits.  COMPATIBILITY: This obviously changes the
-  parsing of some terms, especially where a symbol has been used as a
-  binder, say '\<Pi>x. ...', which is now a type error since \<Pi>x
-  will be parsed as an identifier.  Fix it by inserting a space around
-  former symbols.  Call 'isatool fixgreek' to try to fix parsing
-  errors in existing theory and ML files.
+  (\<aa>...\<zz>\<AA>...\<ZZ>), caligraphic (\<A>...\<Z>), and euler
+  (\<a>...\<z>), are now considered normal letters, and can therefore
+  be used anywhere where an ASCII letter (a...zA...Z) has until
+  now. COMPATIBILITY: This obviously changes the parsing of some
+  terms, especially where a symbol has been used as a binder, say
+  '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed
+  as an identifier.  Fix it by inserting a space around former
+  symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
+  existing theory and ML files.
 
 *** HOL ***
 
diff -r a872d646bf01 -r a3690aeb79d4 src/Pure/General/symbol.ML
--- 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 =