# HG changeset patch
# User wenzelm
# Date 1191859989 -7200
# Node ID 53b20f786a5e723812bb5db5c7eca1256811cf86
# Parent  afae05eb1f1c981e54791df199ecd334a5451df9
avoid polymorphic equality;

diff -r afae05eb1f1c -r 53b20f786a5e src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Mon Oct 08 18:13:08 2007 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Mon Oct 08 18:13:09 2007 +0200
@@ -159,7 +159,7 @@
 
 fun reserved x =
   group ("Reserved identifier " ^ quote x)
-    (Scan.one (T.ident_with (equal x)) >> T.val_of);
+    (Scan.one (T.ident_with (fn y => x = y)) >> T.val_of);
 
 val semicolon = $$$ ";";