# HG changeset patch
# User haftmann
# Date 1125988157 -7200
# Node ID 534b6e5e373663f324ee99988ff57dce54ae89ee
# Parent  c5a52602c4a791ae49f6da84025b2d0c9842646a
eliminated 1 call to polyEq

diff -r c5a52602c4a7 -r 534b6e5e3736 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Mon Sep 05 17:49:28 2005 +0200
+++ b/src/Pure/Isar/outer_keyword.ML	Tue Sep 06 08:29:17 2005 +0200
@@ -83,7 +83,7 @@
 
 (* tags *)
 
-fun update_tags t ts = t :: remove (op =) t ts;
+fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
 
 fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
 fun tags_of (Keyword (_, ts)) = ts;