src/Pure/ML/ml_antiquotation.ML
changeset 78690 e10ef4f9c848
parent 78689 37b49c592265
child 78701 c7b2697094ac
--- a/src/Pure/ML/ml_antiquotation.ML	Sun Sep 24 15:14:45 2023 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Sun Sep 24 15:55:42 2023 +0200
@@ -71,7 +71,7 @@
   ML_Context.add_antiquotation binding true
     (fn _ => fn src => fn ctxt =>
       let
-        val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt;
+        val s = Token.read ctxt Parse.embedded_input src;
         val tokenize = ML_Lex.tokenize_no_range;
         val tokenize_range = ML_Lex.tokenize_range (Input.range_of s);
 
@@ -89,7 +89,7 @@
 fun conditional binding check =
   ML_Context.add_antiquotation binding true
     (fn _ => fn src => fn ctxt =>
-      let val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt in
+      let val s = Token.read ctxt Parse.embedded_input src in
         if check ctxt then ML_Context.read_antiquotes s ctxt
         else (K ([], []), ctxt)
       end);