# 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;