diff -r 3c66b0a9d7b0 -r 73c260342704 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Thu Apr 16 16:19:39 2015 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Thu Apr 16 17:18:48 2015 +0200
@@ -53,15 +53,13 @@
 
   ML_Antiquotation.value @{binding theory}
     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
-      (Context_Position.report ctxt pos
-        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+      (Theory.check ctxt (name, pos);
        "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
     || Scan.succeed "Proof_Context.theory_of ML_context") #>
 
   ML_Antiquotation.value @{binding theory_context}
     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
-      (Context_Position.report ctxt pos
-        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+      (Theory.check ctxt (name, pos);
        "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
         ML_Syntax.print_string name))) #>