diff -r f70e69208a8c -r ceb8a93460b7 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Mar 18 15:29:58 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Mar 18 16:16:28 2014 +0100
@@ -13,10 +13,10 @@
   val thms: xstring -> thm list
   val exec: (unit -> unit) -> Context.generic -> Context.generic
   val check_antiquotation: Proof.context -> xstring * Position.T -> string
+  type decl = Proof.context -> string * string
+  val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
+    theory -> theory
   val print_antiquotations: Proof.context -> unit
-  type decl = Proof.context -> string * string
-  val antiquotation: binding -> 'a context_parser ->
-    (Args.src -> 'a -> Proof.context -> decl * Proof.context) -> theory -> theory
   val trace_raw: Config.raw
   val trace: bool Config.T
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
@@ -80,12 +80,6 @@
   let val (src', f) = Args.check_src ctxt (get_antiquotations ctxt) src
   in f src' ctxt end;
 
-fun antiquotation name scan body =
-  add_antiquotation name
-    (fn src => fn orig_ctxt =>
-      let val (x, _) = Args.syntax scan src orig_ctxt
-      in body src x orig_ctxt end);
-
 
 (* parsing and evaluation *)