--- a/src/Pure/ML/ml_antiquote.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Sun Aug 26 21:46:50 2012 +0200
@@ -71,8 +71,9 @@
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
value (Binding.name "theory")
- (Scan.lift Args.name >> (fn name =>
- "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)
+ (Args.theory -- Scan.lift (Parse.position Args.name) >> (fn (thy, (name, pos)) =>
+ (Position.report pos (Theory.get_markup (Context.get_theory thy name));
+ "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
|| Scan.succeed "Proof_Context.theory_of ML_context") #>
inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>