src/Pure/Isar/method.ML

 
 fun checked_text (Source src) = Token.checked_src src
   | checked_text (Basic _) = true
   | checked_text (Combinator (_, _, body)) = forall checked_text body;
 
+val _ = Theory.setup
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>method\<close>
+    (Args.context -- Scan.lift Args.embedded_position >>
+      (ML_Syntax.print_string o uncurry check_name)));
+
 
 (* method setup *)
 
 fun method_syntax scan src ctxt : method =
   let val (m, ctxt') = Token.syntax scan src ctxt in m ctxt' end;