removed unused operation (reverting 4660b0409096);
authorwenzelm
Mon, 02 Sep 2024 20:12:52 +0200 (4 months ago)
changeset 80802 c3c76f4880bc
parent 80801 090adcdceaae
child 80803 7e39c785ca5d
removed unused operation (reverting 4660b0409096);
src/Pure/General/path.ML
--- 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 *)