tuned signature;

--- a/src/Pure/Isar/keyword.ML	Thu Nov 06 15:47:04 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Nov 06 16:10:33 2014 +0100
@@ -32,7 +32,7 @@
   val prf_asm_goal_script: T
   val prf_script: T
   type spec = (string * string list) * string list
-  val spec: spec -> T
+  val check_spec: spec -> T
   val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
   type keywords
   val minor_keywords: keywords -> Scan.lexicon
@@ -112,14 +112,14 @@
 
 type spec = (string * string list) * string list;
 
-fun spec ((kind, files), tags) =
+fun check_spec ((kind, files), tags) =
   if not (member (op =) kinds kind) then
     error ("Unknown outer syntax keyword kind " ^ quote kind)
   else if not (null files) andalso kind <> kind_of thy_load then
     error ("Illegal specification of files for " ^ quote kind)
   else Keyword {kind = kind, files = files, tags = tags};
 
-fun command_spec ((name, s), pos) = ((name, spec s), pos);
+fun command_spec ((name, s), pos) = ((name, check_spec s), pos);
 
 
 

--- a/src/Pure/Thy/thy_header.ML	Thu Nov 06 15:47:04 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Thu Nov 06 16:10:33 2014 +0100
@@ -38,7 +38,7 @@
 (** keyword declarations **)
 
 fun define_keywords (keywords: keywords) =
-  List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
+  List.app (Keyword.define o apsnd (Option.map Keyword.check_spec)) keywords;
 
 fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);
 
@@ -52,7 +52,7 @@
 
 fun declare_keyword (name, spec) =
   Data.map (fn data =>
-    (Option.map Keyword.spec spec;
+    (Option.map Keyword.check_spec spec;
       Symtab.update_new (name, spec) data handle Symtab.DUP dup => err_dup dup));
 
 fun the_keyword thy name =