# HG changeset patch
# User wenzelm
# Date 1554147913 -7200
# Node ID 0cb334eee651a64cb82d6157580d61aa497e8459
# Parent  095dce9892e8bba888d6794b774a40c928280be6
tuned signature;

diff -r 095dce9892e8 -r 0cb334eee651 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Mon Apr 01 17:02:43 2019 +0100
+++ b/src/Pure/General/path.ML	Mon Apr 01 21:45:13 2019 +0200
@@ -41,7 +41,7 @@
   eqtype binding
   val binding: T * Position.T -> binding
   val binding0: T -> binding
-  val binding_map: (T -> T) -> binding -> binding
+  val map_binding: (T -> T) -> binding -> binding
   val dest_binding: binding -> T * Position.T
   val implode_binding: binding -> string
   val explode_binding: string * Position.T -> binding
@@ -264,7 +264,8 @@
   else error ("Bad path binding: " ^ print path ^ Position.here pos);
 
 fun binding0 path = binding (path, Position.none);
-fun binding_map f (Binding (path, pos)) = binding (f path, pos);
+
+fun map_binding f (Binding (path, pos)) = binding (f path, pos);
 
 fun dest_binding (Binding args) = args;