--- a/src/Pure/General/path.ML Mon Sep 02 15:23:12 2024 +0200
+++ b/src/Pure/General/path.ML Mon Sep 02 20:12:52 2024 +0200
@@ -25,7 +25,6 @@
val implode: T -> string
val explode: string -> T
val explode_pos: string * Position.T -> T * Position.T
- val decode: T XML.Decode.T
val split: string -> T list
val pretty: T -> Pretty.T
val print: T -> string
@@ -186,8 +185,6 @@
space_explode ":" str
|> map_filter (fn s => if s = "" then NONE else SOME (explode_path s));
-val decode = XML.Decode.string #> explode_path;
-
(* print *)