# HG changeset patch
# User kleing
# Date 1066175567 -7200
# Node ID ef550525c591bd8d9ee823147dd0834a58e2cf70
# Parent  6d8b6eb8623b72871b8b3b97511bd8e30b99b02c
included \<^sub> in the range of identifier chars

diff -r 6d8b6eb8623b -r ef550525c591 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Oct 13 16:54:20 2003 +0200
+++ b/src/Pure/General/symbol.ML	Wed Oct 15 01:52:47 2003 +0200
@@ -110,13 +110,17 @@
 
     val bbb_letters = ["bool","complex","nat","rat","real","int"]
 
+    val control_letters = ["^sub"]
+ 
     val pre_letters =
 	cal_letters   @
 	small_letters @
 	goth_letters  @
-	greek_letters
+	greek_letters @
+	control_letters
+
 in
-val ext_letters = map wrap pre_letters
+val ext_letters = map wrap pre_letters 
 
 fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters
 end