src/Pure/ML/ml_antiquotations.ML
changeset 58932 5fd496c26e3b
parent 58928 23d0ffd48006
child 58978 e42da880c61e
--- 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;