# HG changeset patch
# User wenzelm
# Date 1554326959 -7200
# Node ID 198bbe73b1006c4380cd9de3c72a489abe8910ba
# Parent  96fe857a7a6f598dde6a14ba27fc1cb19930327a
tuned signature;

diff -r 96fe857a7a6f -r 198bbe73b100 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed Apr 03 21:50:00 2019 +0200
+++ b/src/Pure/General/path.ML	Wed Apr 03 23:29:19 2019 +0200
@@ -43,6 +43,8 @@
   val binding0: T -> binding
   val map_binding: (T -> T) -> binding -> binding
   val dest_binding: binding -> T * Position.T
+  val path_of_binding: binding -> T
+  val pos_of_binding: binding -> Position.T
   val implode_binding: binding -> string
   val explode_binding: string * Position.T -> binding
   val explode_binding0: string -> binding
@@ -268,8 +270,10 @@
 fun map_binding f (Binding (path, pos)) = binding (f path, pos);
 
 fun dest_binding (Binding args) = args;
+val path_of_binding = dest_binding #> #1;
+val pos_of_binding = dest_binding #> #2;
 
-val implode_binding = dest_binding #> #1 #> implode_path;
+val implode_binding = path_of_binding #> implode_path;
 
 val explode_binding = binding o explode_pos;
 fun explode_binding0 s = explode_binding (s, Position.none);