diff -r a2c589d5e1e4 -r 2f6855142a8c src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Fri Apr 09 21:07:11 2021 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Fri Apr 09 22:06:59 2021 +0200
@@ -18,6 +18,7 @@
   val inline_embedded: binding -> string context_parser -> theory -> theory
   val value: binding -> string context_parser -> theory -> theory
   val value_embedded: binding -> string context_parser -> theory -> theory
+  val special_form: binding -> string -> theory -> theory
 end;
 
 structure ML_Antiquotation: ML_ANTIQUOTATION =
@@ -63,6 +64,26 @@
 end;
 
 
+(* ML special form *)
+
+fun special_form binding operator =
+  ML_Context.add_antiquotation binding true
+    (fn _ => fn src => fn ctxt =>
+      let
+        val (s, _) = Token.syntax (Scan.lift Args.embedded_input) src ctxt;
+        val tokenize = ML_Lex.tokenize_range Position.no_range;
+        val tokenize_range = ML_Lex.tokenize_range (Input.range_of s);
+        fun decl (_: Proof.context) =
+          let
+            val expr = ML_Lex.read_source s |> map Antiquote.the_text;
+            val ml =
+              tokenize "let val expr = (fn () => " @ expr @ tokenize ");" @
+              tokenize " val " @ tokenize_range "result" @
+              tokenize (" = " ^ operator ^ " expr; in result end")
+          in ([], ml) end;
+      in (decl, ctxt) end);
+
+
 (* basic antiquotations *)
 
 val _ = Theory.setup