diff -r f0cb320603cb -r 30bcf149054d src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Oct 22 19:40:28 2023 +0200
+++ b/src/Pure/Isar/parse.ML	Mon Oct 23 12:08:38 2023 +0200
@@ -147,22 +147,8 @@
 
 (* cut *)
 
-fun cut kind scan =
-  let
-    fun get_pos [] = " (end-of-input)"
-      | get_pos (tok :: _) = Position.here (Token.pos_of tok);
-
-    fun err (toks, NONE) = (fn () => kind ^ get_pos toks)
-      | err (toks, SOME msg) =
-          (fn () =>
-            let val s = msg () in
-              if String.isPrefix kind s then s
-              else kind ^ get_pos toks ^ ": " ^ s
-            end);
-  in Scan.!! err scan end;
-
-fun !!! scan = cut "Outer syntax error" scan;
-fun !!!! scan = cut "Corrupted outer syntax in presentation" scan;
+fun !!! scan = Scan.!!! "Outer syntax error" Token.input_position scan;
+fun !!!! scan = Scan.!!! "Corrupted outer syntax in presentation" Token.input_position scan;