# HG changeset patch
# User wenzelm
# Date 1331749635 -3600
# Node ID f2c60ad58374d52a89616865163cd4fbda15ee52
# Parent  947f630620222df1f37e71c8cf10e5e87f12a7b9
tuned;

diff -r 947f63062022 -r f2c60ad58374 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Wed Mar 14 18:09:05 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Wed Mar 14 19:27:15 2012 +0100
@@ -32,7 +32,6 @@
   val prf_asm_goal: T
   val prf_script: T
   val kinds: string list
-  val update_tags: string -> string list -> string list
   val tag: string -> T -> T
   val tags_of: T -> string list
   val tag_theory: T -> T
@@ -108,9 +107,7 @@
 
 (* tags *)
 
-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 tag t (Keyword (s, ts)) = Keyword (s, update (op =) t ts);
 fun tags_of (Keyword (_, ts)) = ts;
 
 val tag_theory = tag "theory";
diff -r 947f63062022 -r f2c60ad58374 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Mar 14 18:09:05 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Mar 14 19:27:15 2012 +0100
@@ -291,7 +291,7 @@
     val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
 
     val (tag, tags) = tag_stack;
-    val tag' = try hd (fold Keyword.update_tags cmd_tags (the_list tag));
+    val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
 
     val active_tag' =
       if is_some tag' then tag'