added is_current;

--- a/src/Pure/General/path.ML	Tue Apr 20 15:23:43 1999 +0200
+++ b/src/Pure/General/path.ML	Wed Apr 21 16:30:35 1999 +0200
@@ -10,6 +10,7 @@
   datatype elem = Root | Parent | Basic of string | Variable of string
   eqtype T
   val rep: T -> elem list
+  val is_current: T -> bool
   val current: T
   val root: T
   val parent: T
@@ -59,6 +60,9 @@
 
 fun rep (Path xs) = xs;
 
+fun is_current (Path []) = true
+  | is_current _ = false;
+
 val current = Path [];
 val root = Path [Root];
 val parent = Path [Parent];