# HG changeset patch
# User wenzelm
# Date 1415378630 -3600
# Node ID 5fd496c26e3b9fe39695bea5912e51e970c9352b
# Parent  3097ec6535477aaff7b42842e61312937cb3c67f
tuned;

diff -r 3097ec653547 -r 5fd496c26e3b src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Fri Nov 07 17:31:01 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Fri Nov 07 17:43:50 2014 +0100
@@ -233,20 +233,17 @@
 
 (* outer syntax *)
 
-fun with_keyword f =
-  Args.theory -- Scan.lift (Parse.position Parse.string)
-    >> (fn (thy, (name, pos)) => (f (name, pos, Thy_Header.the_keyword thy (name, pos))));
-
 val _ = Theory.setup
  (ML_Antiquotation.value @{binding keyword}
-    (with_keyword (fn (name, pos, is_command) =>
-      if not is_command then "Parse.$$$ " ^ ML_Syntax.print_string name
-      else error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
+    (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
+      if Keyword.is_keyword (Thy_Header.get_keywords thy) name then
+        "Parse.$$$ " ^ ML_Syntax.print_string name
+      else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
   ML_Antiquotation.value @{binding command_spec}
-    (with_keyword (fn (name, pos, is_command) =>
-      if is_command then
+    (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
+      if Keyword.is_command (Thy_Header.get_keywords thy) name then
         ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)
-      else error ("Expected command keyword " ^ quote name ^ Position.here pos))));
+      else error ("Bad outer syntax command " ^ quote name ^ Position.here pos))));
 
 end;
 
diff -r 3097ec653547 -r 5fd496c26e3b src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Fri Nov 07 17:31:01 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Fri Nov 07 17:43:50 2014 +0100
@@ -16,7 +16,6 @@
   val add_keywords: keywords -> theory -> theory
   val get_keywords: theory -> Keyword.keywords
   val get_keywords': Proof.context -> Keyword.keywords
-  val the_keyword: theory -> string * Position.T -> bool
   val args: header parser
   val read: Position.T -> string -> header
   val read_tokens: Token.T list -> header
@@ -90,13 +89,6 @@
 val get_keywords = Data.get;
 val get_keywords' = get_keywords o Proof_Context.theory_of;
 
-fun the_keyword thy (name, pos) =
-  let val keywords = get_keywords thy in
-    if Keyword.is_literal keywords name
-    then Keyword.is_command keywords name
-    else error ("Undeclared outer syntax keyword " ^ quote name ^ Position.here pos)
-  end;
-
 
 
 (** concrete syntax **)