src/Pure/General/path.ML

--- a/src/Pure/General/path.ML	Fri Apr 11 09:36:38 2014 +0200
+++ b/src/Pure/General/path.ML	Fri Apr 11 11:52:28 2014 +0200
@@ -17,6 +17,7 @@
   val variable: string -> T
   val is_absolute: T -> bool
   val is_basic: T -> bool
+  val starts_basic: T -> bool
   val append: T -> T -> T
   val appends: T list -> T
   val make: string list -> T
@@ -93,6 +94,11 @@
 fun is_basic (Path [Basic _]) = true
   | is_basic _ = false;
 
+fun starts_basic (Path xs) =
+  (case try List.last xs of
+    SOME (Basic _) => true
+  | _ => false);
+
 
 (* append and norm *)