tuned signature;

--- a/src/Pure/Isar/keyword.ML	Thu Nov 06 13:36:19 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Nov 06 13:44:14 2014 +0100
@@ -37,10 +37,10 @@
   type keywords
   val minor_keywords: keywords -> Scan.lexicon
   val major_keywords: keywords -> Scan.lexicon
+  val no_command_keywords: keywords -> keywords
   val empty_keywords: keywords
   val merge_keywords: keywords * keywords -> keywords
-  val no_command_keywords: keywords -> keywords
-  val add: string * T option -> keywords -> keywords
+  val add_keywords: string * T option -> keywords -> keywords
   val define: string * T option -> unit
   val get_keywords: unit -> keywords
   val is_keyword: keywords -> string -> bool
@@ -142,6 +142,12 @@
 fun map_keywords f (Keywords {minor, major, commands}) =
   make_keywords (f (minor, major, commands));
 
+val no_command_keywords =
+  map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));
+
+
+(* build keywords *)
+
 val empty_keywords =
   make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty);
 
@@ -153,13 +159,7 @@
     Scan.merge_lexicons (major1, major2),
     Symtab.merge (K true) (commands1, commands2));
 
-val no_command_keywords =
-  map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));
-
-
-(* add keywords *)
-
-fun add (name, opt_kind) = map_keywords (fn (minor, major, commands) =>
+fun add_keywords (name, opt_kind) = map_keywords (fn (minor, major, commands) =>
   (case opt_kind of
     NONE =>
       let
@@ -176,7 +176,7 @@
 
 local val global_keywords = Unsynchronized.ref empty_keywords in
 
-fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add decl));
+fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add_keywords decl));
 fun get_keywords () = ! global_keywords;
 
 end;

--- a/src/Pure/Thy/thy_header.ML	Thu Nov 06 13:36:19 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Thu Nov 06 13:44:14 2014 +0100
@@ -79,9 +79,9 @@
 
 val header_keywords =
   Keyword.empty_keywords
-  |> fold (Keyword.add o rpair NONE)
+  |> fold (Keyword.add_keywords o rpair NONE)
     ["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN]
-  |> fold Keyword.add
+  |> fold Keyword.add_keywords
     [(headerN, SOME Keyword.heading),
      (chapterN, SOME Keyword.heading),
      (sectionN, SOME Keyword.heading),

--- a/src/Pure/Tools/find_consts.ML	Thu Nov 06 13:36:19 2014 +0100
+++ b/src/Pure/Tools/find_consts.ML	Thu Nov 06 13:44:14 2014 +0100
@@ -140,7 +140,7 @@
 
 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
 
-val query_keywords = Keyword.add (":", NONE) Keyword.empty_keywords;
+val query_keywords = Keyword.add_keywords (":", NONE) Keyword.empty_keywords;
 
 in
 

--- a/src/Pure/Tools/find_theorems.ML	Thu Nov 06 13:36:19 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Thu Nov 06 13:44:14 2014 +0100
@@ -526,7 +526,7 @@
 
 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
 
-val query_keywords = Keyword.add (":", NONE) Keyword.empty_keywords;
+val query_keywords = Keyword.add_keywords (":", NONE) Keyword.empty_keywords;
 
 in