--- a/src/Pure/Isar/parse.ML Fri Oct 20 11:03:09 2023 +0200
+++ b/src/Pure/Isar/parse.ML Fri Oct 20 16:40:41 2023 +0200
@@ -123,7 +123,6 @@
val embedded_ml: ML_Lex.token Antiquote.antiquote list parser
val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
val read_embedded: Proof.context -> Keyword.keywords -> 'a parser -> Input.source -> 'a
- val read_embedded_src: Proof.context -> Keyword.keywords -> 'a parser -> Token.src -> 'a
end;
structure Parse: PARSE =
@@ -533,8 +532,4 @@
| NONE => error ("Bad input" ^ Position.here (Input.pos_of input)))
end;
-fun read_embedded_src ctxt keywords parse src =
- Token.read ctxt embedded_input src
- |> read_embedded ctxt keywords parse;
-
end;