# HG changeset patch
# User wenzelm
# Date 1698055899 -7200
# Node ID aff231884b20bbbd51356232749fe7086188cda0
# Parent  30bcf149054d35308a686da9da4795329ef5c176
unused (see fe9e590ae52f);

diff -r 30bcf149054d -r aff231884b20 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Mon Oct 23 12:08:38 2023 +0200
+++ b/src/Pure/Isar/parse.ML	Mon Oct 23 12:11:39 2023 +0200
@@ -8,7 +8,6 @@
 sig
   val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
   val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
-  val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
   val not_eof: Token.T parser
   val token: 'a parser -> Token.T parser
   val range: 'a parser -> ('a * Position.range) parser
@@ -148,7 +147,6 @@
 (* cut *)
 
 fun !!! scan = Scan.!!! "Outer syntax error" Token.input_position scan;
-fun !!!! scan = Scan.!!! "Corrupted outer syntax in presentation" Token.input_position scan;