# HG changeset patch
# User wenzelm
# Date 1629625657 -7200
# Node ID 7b93dc3f2b34d4efb1514d55b2fa37edaa4dae5a
# Parent  afe3c8ae1624b50a8305b5c0e88f1ab683fa9fdf
tuned;

diff -r afe3c8ae1624 -r 7b93dc3f2b34 src/Pure/ML/ml_antiquotations2.ML
--- a/src/Pure/ML/ml_antiquotations2.ML	Sat Aug 21 20:12:15 2021 +0000
+++ b/src/Pure/ML/ml_antiquotations2.ML	Sun Aug 22 11:47:37 2021 +0200
@@ -9,12 +9,11 @@
 
 val _ = Theory.setup
  (ML_Antiquotation.inline_embedded \<^binding>\<open>method\<close>
-    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
-      ML_Syntax.print_string (Method.check_name ctxt (name, pos)))) #>
+    (Args.context -- Scan.lift Args.embedded_position >>
+      (ML_Syntax.print_string o uncurry Method.check_name)) #>
 
   ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close>
-   (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
-      Locale.check (Proof_Context.theory_of ctxt) (name, pos)
-      |> ML_Syntax.print_string)));
+   (Args.theory -- Scan.lift Args.embedded_position >>
+      (ML_Syntax.print_string o uncurry Locale.check)));
 
 end;