diff -r a884b2967dd7 -r 36fb663145e5 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Thu Apr 04 16:47:09 2019 +0200
+++ b/src/Pure/General/path.ML	Thu Apr 04 20:45:55 2019 +0200
@@ -45,6 +45,7 @@
   val dest_binding: binding -> T * Position.T
   val path_of_binding: binding -> T
   val pos_of_binding: binding -> Position.T
+  val proper_binding: binding -> unit
   val implode_binding: binding -> string
   val explode_binding: string * Position.T -> binding
   val explode_binding0: string -> binding
@@ -262,7 +263,7 @@
 datatype binding = Binding of T * Position.T;
 
 fun binding (path, pos) =
-  if not (is_current path) andalso all_basic path then Binding (path, pos)
+  if all_basic path then Binding (path, pos)
   else error ("Bad path binding: " ^ print path ^ Position.here pos);
 
 fun binding0 path = binding (path, Position.none);
@@ -273,6 +274,11 @@
 val path_of_binding = dest_binding #> #1;
 val pos_of_binding = dest_binding #> #2;
 
+fun proper_binding binding =
+  if is_current (path_of_binding binding)
+  then error ("Empty path" ^ Position.here (pos_of_binding binding))
+  else ();
+
 val implode_binding = path_of_binding #> implode_path;
 
 val explode_binding = binding o explode_pos;