clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
subtle change of semantics of ML_Context.add_antiq: need to avoid accidental update of context due to concrete syntax parser (cf. Scan.pass);

--- a/src/Pure/ML/ml_antiquote.ML	Fri Aug 23 17:01:12 2013 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Fri Aug 23 19:53:27 2013 +0200
@@ -7,9 +7,7 @@
 signature ML_ANTIQUOTE =
 sig
   val variant: string -> Proof.context -> string * Proof.context
-  val macro: binding -> Proof.context context_parser -> theory -> theory
   val inline: binding -> string context_parser -> theory -> theory
-  val declaration: string -> binding -> string context_parser -> theory -> theory
   val value: binding -> string context_parser -> theory -> theory
 end;
 
@@ -38,23 +36,20 @@
 
 (* specific antiquotations *)
 
-fun macro name scan = ML_Context.add_antiq name
-  (fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
-    (Context.Proof ctxt, fn background => (K ("", ""), background)))));
-
-fun inline name scan = ML_Context.add_antiq name
-  (fn _ => scan >> (fn s => fn background => (K ("", s), background)));
+fun inline name scan =
+  ML_Context.add_antiq name
+    (Scan.depend (fn context => Scan.pass context scan >> (fn s => (context, K ("", s)))));
 
-fun declaration kind name scan = ML_Context.add_antiq name
-  (fn _ => scan >> (fn s => fn background =>
-    let
-      val (a, background') =
-        variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) background;
-      val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
-      val body = "Isabelle." ^ a;
-    in (K (env, body), background') end));
-
-val value = declaration "val";
+fun value name scan =
+  ML_Context.add_antiq name
+    (Scan.depend (fn context => Scan.pass context scan >> (fn s =>
+      let
+        val ctxt = Context.the_proof context;
+        val (a, ctxt') =
+          variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) ctxt;
+        val env = "val " ^ a ^ " = " ^ s ^ ";\n";
+        val body = "Isabelle." ^ a;
+      in (Context.Proof ctxt', (K (env, body))) end)));
 
 
 

--- a/src/Pure/ML/ml_context.ML	Fri Aug 23 17:01:12 2013 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Aug 23 19:53:27 2013 +0200
@@ -23,8 +23,8 @@
   val get_stored_thm: unit -> thm
   val ml_store_thms: string * thm list -> unit
   val ml_store_thm: string * thm -> unit
-  type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context
-  val add_antiq: binding -> (Position.T -> antiq context_parser) -> theory -> theory
+  type antiq = Proof.context -> string * string
+  val add_antiq: binding -> antiq context_parser -> theory -> theory
   val check_antiq: theory -> xstring * Position.T -> string
   val trace_raw: Config.raw
   val trace: bool Config.T
@@ -97,11 +97,11 @@
 
 (* antiquotation commands *)
 
-type antiq = Proof.context -> (Proof.context -> string * string) * Proof.context;
+type antiq = Proof.context -> string * string;
 
 structure Antiq_Parsers = Theory_Data
 (
-  type T = (Position.T -> antiq context_parser) Name_Space.table;
+  type T = antiq context_parser Name_Space.table;
   val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
   val extend = I;
   fun merge data : T = Name_Space.merge_tables data;
@@ -117,7 +117,7 @@
     val thy = Proof_Context.theory_of ctxt;
     val ((xname, _), pos) = Args.dest_src src;
     val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos);
-  in Args.context_syntax Markup.ML_antiquotationN (scan pos) src ctxt end;
+  in Args.context_syntax Markup.ML_antiquotationN scan src ctxt end;
 
 
 (* parsing and evaluation *)
@@ -160,9 +160,7 @@
           fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
             | expand (Antiquote.Antiq (ss, range)) ctxt =
                 let
-                  val (f, _) =
-                    antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
-                  val (decl, ctxt') = f ctxt;  (* FIXME ?? *)
+                  val (decl, ctxt') = antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
                   val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
                 in (decl', ctxt') end;
 

--- a/src/Pure/ML/ml_thms.ML	Fri Aug 23 17:01:12 2013 +0200
+++ b/src/Pure/ML/ml_thms.ML	Fri Aug 23 19:53:27 2013 +0200
@@ -37,43 +37,50 @@
 val _ =
   Context.>> (Context.map_theory
     (ML_Context.add_antiq (Binding.name "attributes")
-      (fn _ => Scan.lift Parse_Spec.attribs >> (fn raw_srcs => fn background =>
+      (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
         let
-          val thy = Proof_Context.theory_of background;
+          val ctxt = Context.the_proof context;
+          val thy = Proof_Context.theory_of ctxt;
 
           val i = serial ();
           val srcs = map (Attrib.intern_src thy) raw_srcs;
-          val _ = map (Attrib.attribute background) srcs;
-          val (a, background') = background
+          val _ = map (Attrib.attribute ctxt) srcs;
+          val (a, ctxt') = ctxt
             |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
           val ml =
             ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
               string_of_int i ^ ";\n", "Isabelle." ^ a);
-        in (K ml, background') end))));
+        in (Context.Proof ctxt', K ml) end)))));
 
 
 (* fact references *)
 
-fun thm_binding kind is_single thms background =
+fun thm_binding kind is_single context thms =
   let
-    val initial = null (get_thmss background);
-    val (name, background') = ML_Antiquote.variant kind background;
-    val background'' = cons_thms ((name, is_single), thms) background';
+    val ctxt = Context.the_proof context;
+
+    val initial = null (get_thmss ctxt);
+    val (name, ctxt') = ML_Antiquote.variant kind ctxt;
+    val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
 
     val ml_body = "Isabelle." ^ name;
-    fun decl ctxt =
+    fun decl final_ctxt =
       if initial then
         let
-          val binds = get_thmss ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a);
+          val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a);
           val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n";
         in (ml_env, ml_body) end
       else ("", ml_body);
-  in (decl, background'') end;
+  in (Context.Proof ctxt'', decl) end;
 
 val _ =
   Context.>> (Context.map_theory
-   (ML_Context.add_antiq (Binding.name "thm") (K (Attrib.thm >> (thm_binding "thm" true o single))) #>
-    ML_Context.add_antiq (Binding.name "thms") (K (Attrib.thms >> thm_binding "thms" false))));
+    (ML_Context.add_antiq (Binding.name "thm")
+      (Scan.depend (fn context =>
+        Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
+     ML_Context.add_antiq (Binding.name "thms")
+      (Scan.depend (fn context =>
+        Scan.pass context Attrib.thms >> thm_binding "thms" false context))));
 
 
 (* ad-hoc goals *)
@@ -85,24 +92,26 @@
 val _ =
   Context.>> (Context.map_theory
    (ML_Context.add_antiq (Binding.name "lemma")
-    (fn _ => Args.context --
-        Scan.lift (Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) --
-          (by |-- Method.parse -- Scan.option Method.parse)) >>
-      (fn (ctxt, ((is_open, raw_propss), methods)) =>
-        let
-          val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
-          val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
-          fun after_qed res goal_ctxt =
-            Proof_Context.put_thms false (Auto_Bind.thisN,
-              SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
+    (Scan.depend (fn context =>
+      Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) --
+      (by |-- Method.parse -- Scan.option Method.parse) >>
+        (fn ((is_open, raw_propss), methods) =>
+          let
+            val ctxt = Context.proof_of context;
 
-          val ctxt' = ctxt
-            |> Proof.theorem NONE after_qed propss
-            |> Proof.global_terminal_proof methods;
-          val thms =
-            Proof_Context.get_fact ctxt'
-              (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
-        in thm_binding "lemma" (length (flat propss) = 1) thms end))));
+            val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
+            val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
+            fun after_qed res goal_ctxt =
+              Proof_Context.put_thms false (Auto_Bind.thisN,
+                SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
+
+            val ctxt' = ctxt
+              |> Proof.theorem NONE after_qed propss
+              |> Proof.global_terminal_proof methods;
+            val thms =
+              Proof_Context.get_fact ctxt'
+                (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
+          in thm_binding "lemma" (length (flat propss) = 1) context thms end)))));
 
 end;
 

--- a/src/Tools/Code/code_runtime.ML	Fri Aug 23 17:01:12 2013 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Aug 23 19:53:27 2013 +0200
@@ -247,12 +247,15 @@
 
 in
 
-fun ml_code_antiq raw_const background =
+fun ml_code_antiq context raw_const =
   let
-    val const = Code.check_const (Proof_Context.theory_of background) raw_const;
-    val is_first = is_first_occ background;
-    val background' = register_const const background;
-  in (print_code is_first const, background') end;
+    val ctxt = Context.the_proof context;
+    val thy = Proof_Context.theory_of ctxt;
+
+    val const = Code.check_const thy raw_const;
+    val is_first = is_first_occ ctxt;
+    val ctxt' = register_const const ctxt;
+  in (Context.Proof ctxt', print_code is_first const) end;
 
 end; (*local*)
 
@@ -344,7 +347,8 @@
 
 val _ =
   Context.>> (Context.map_theory
-    (ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq)));
+    (ML_Context.add_antiq @{binding code}
+      (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context))));
 
 local