src/Pure/General/symbol.scala
changeset 44331 8a6de1a6e1dc
parent 44330 4b4b93672f15
child 44358 98cd7e83fc5b
     1.1 --- a/src/Pure/General/symbol.scala	Sun Jun 19 14:11:06 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Sun Jun 19 14:31:08 2011 +0200
     1.3 @@ -230,7 +230,7 @@
     1.4  
     1.5      val names: Map[String, String] =
     1.6      {
     1.7 -      val name = new Regex("""\\<([A-Za-z][A-Za-z0-9_']*)>""")
     1.8 +      val name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
     1.9        Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
    1.10      }
    1.11