diff -r 5f3f203a38ad -r 74eddfef841e src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Mon Sep 14 16:44:09 2015 +0200 +++ b/src/Pure/General/symbol.scala Mon Sep 14 17:39:29 2015 +0200 @@ -289,7 +289,7 @@ props match { case Nil => Nil case _ :: Nil => err() - case Key(x) :: y :: rest => (x -> y) :: read_props(rest) + case Key(x) :: y :: rest => (x -> y.replace('\u2423', ' ')) :: read_props(rest) case _ => err() } }