# HG changeset patch
# User wenzelm
# Date 1289297835 -3600
# Node ID 27c1a1c82eba77691b94fa5bc06d1f3a87295cba
# Parent  65bd37d7d5010d8e158214887539a3afa1da8a65# Parent  020c16837866a96f797c61079d90a1e6ce89b8d9
merged

diff -r 65bd37d7d501 -r 27c1a1c82eba etc/symbols
--- a/etc/symbols	Mon Nov 08 23:02:20 2010 +0100
+++ b/etc/symbols	Tue Nov 09 11:17:15 2010 +0100
@@ -181,7 +181,7 @@
 \<downharpoonleft>      code: 0x0021c3  font: Isabelle
 \<downharpoonright>     code: 0x0021c2  font: Isabelle
 \<upharpoonleft>        code: 0x0021bf  font: Isabelle
-\<upharpoonright>       code: 0x0021be  font: Isabelle
+#\<upharpoonright>       code: 0x0021be  font: Isabelle
 \<restriction>          code: 0x0021be  font: Isabelle
 \<Colon>                code: 0x002237  font: Isabelle
 \<up>                   code: 0x002191  font: Isabelle
diff -r 65bd37d7d501 -r 27c1a1c82eba src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Nov 08 23:02:20 2010 +0100
+++ b/src/Pure/General/symbol.scala	Tue Nov 09 11:17:15 2010 +0100
@@ -146,7 +146,18 @@
       }
       (min, max)
     }
-    private val table = Map[String, String]() ++ list
+    private val table =
+    {
+      var tab = Map[String, String]()
+      for ((x, y) <- list) {
+        tab.get(x) match {
+          case None => tab += (x -> y)
+          case Some(z) =>
+            error("Duplicate mapping of \"" + x + "\" to \"" + y + "\" vs. \"" + z + "\"")
+        }
+      }
+      tab
+    }
     def recode(text: String): String =
     {
       val len = text.length
@@ -198,8 +209,9 @@
     }
 
     private val symbols: List[(String, Map[String, String])] =
-      for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
-        yield read_decl(decl)
+      Map((
+        for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
+          yield read_decl(decl)): _*) toList
 
 
     /* misc properties */
@@ -210,9 +222,10 @@
       Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
     }
 
-    val abbrevs: Map[String, String] = Map((
-      for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
-        yield (sym -> props("abbrev"))): _*)
+    val abbrevs: Map[String, String] =
+      Map((
+        for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
+          yield (sym -> props("abbrev"))): _*)
 
 
     /* main recoder methods */