src/Pure/Isar/parse.ML

--- a/src/Pure/Isar/parse.ML	Thu Oct 21 18:10:51 2021 +0200
+++ b/src/Pure/Isar/parse.ML	Thu Oct 21 18:20:08 2021 +0200
@@ -514,23 +514,16 @@
 
 (* read embedded source, e.g. for antiquotations *)
 
+fun tokenize keywords = Token.tokenize keywords {strict = true} #> filter Token.is_proper;
+
 fun read_antiq keywords scan (syms, pos) =
-  let
-    val toks = syms
-      |> Token.tokenize (Keyword.no_command_keywords keywords) {strict = true}
-      |> filter Token.is_proper;
-  in
-    (case Scan.read Token.stopper scan toks of
-      SOME res => res
-    | NONE => error ("Malformed antiquotation" ^ Position.here pos))
-  end;
+  (case Scan.read Token.stopper scan (tokenize (Keyword.no_command_keywords keywords) syms) of
+    SOME res => res
+  | NONE => error ("Malformed antiquotation" ^ Position.here pos));
 
 fun read_embedded ctxt keywords parse input =
   let
-    val toks = input
-      |> Input.source_explode
-      |> Token.tokenize keywords {strict = true}
-      |> filter Token.is_proper;
+    val toks = tokenize keywords (Input.source_explode input);
     val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
   in
     (case Scan.read Token.stopper parse toks of