author | wenzelm |
Thu, 21 Jan 2016 22:16:48 +0100 | |
changeset 62230 | 949d2c9f6ff7 |
parent 62229 | 027e6032977f |
child 62231 | 25f4a9cd8b68 |
--- a/src/Pure/General/symbol.scala Thu Jan 21 21:12:45 2016 +0100 +++ b/src/Pure/General/symbol.scala Thu Jan 21 22:16:48 2016 +0100 @@ -255,7 +255,7 @@ tab.get(x) match { case None => tab += (x -> y) case Some(z) => - error("Duplicate mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z)) + error("Duplicate symbol mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z)) } } tab