| changeset 62230 | 949d2c9f6ff7 |
| parent 62104 | fb73c0d7bb37 |
| child 62528 | c8c532b22947 |
--- 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