# HG changeset patch
# User wenzelm
# Date 1725300772 -7200
# Node ID c3c76f4880bc02fb0aa75d773a227285cea75809
# Parent  090adcdceaaefc77057e698d23fff3ae6f89263e
removed unused operation (reverting 4660b0409096);

diff -r 090adcdceaae -r c3c76f4880bc 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 *)