merged

--- a/doc-src/pdfsetup.sty	Tue Nov 09 13:59:37 2010 +0000
+++ b/doc-src/pdfsetup.sty	Tue Nov 09 14:00:10 2010 +0000
@@ -15,6 +15,9 @@
 \urlstyle{rm}
 \ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
 
+\def\isaliteral#1#2{#2}
+\def\isanil{}
+
 \ifpdf
 \ifnum\pdfminorversion<5\pdfminorversion=5\fi
 \renewcommand{\isaliteral}[2]{%

--- a/etc/symbols	Tue Nov 09 13:59:37 2010 +0000
+++ b/etc/symbols	Tue Nov 09 14:00:10 2010 +0000
@@ -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

--- a/src/Pure/General/symbol.scala	Tue Nov 09 13:59:37 2010 +0000
+++ b/src/Pure/General/symbol.scala	Tue Nov 09 14:00:10 2010 +0000
@@ -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 */