--- 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 *)