| changeset 78690 | e10ef4f9c848 |
| parent 76614 | ac08b6e3b9e3 |
| child 78804 | d4e9d6b7f48d |
--- a/src/Pure/Isar/parse.ML Sun Sep 24 15:14:45 2023 +0200 +++ b/src/Pure/Isar/parse.ML Sun Sep 24 15:55:42 2023 +0200 @@ -534,7 +534,7 @@ end; fun read_embedded_src ctxt keywords parse src = - Token.syntax (Scan.lift embedded_input) src ctxt - |> #1 |> read_embedded ctxt keywords parse; + Token.read ctxt embedded_input src + |> read_embedded ctxt keywords parse; end;