reject path variable nesting explicitly;

--- a/src/Pure/General/path.ML	Fri Aug 03 12:37:31 2012 +0200
+++ b/src/Pure/General/path.ML	Fri Aug 03 13:06:25 2012 +0200
@@ -179,7 +179,12 @@
 
 (* expand variables *)
 
-fun eval (Variable s) = rep (explode_path (getenv_strict s))
+fun eval (Variable s) =
+      let val path = explode_path (getenv_strict s) in
+        if exists (fn Variable _ => true | _ => false) (rep path) then
+          error ("Illegal path variable nesting: " ^ s ^ "=" ^ print path)
+        else rep path
+      end
   | eval x = [x];
 
 val expand = rep #> maps eval #> norm #> Path;

--- a/src/Pure/General/path.scala	Fri Aug 03 12:37:31 2012 +0200
+++ b/src/Pure/General/path.scala	Fri Aug 03 13:06:25 2012 +0200
@@ -167,7 +167,10 @@
     def eval(elem: Path.Elem): List[Path.Elem] =
       elem match {
         case Path.Variable(s) =>
-          Path.explode(Isabelle_System.getenv_strict(s)).elems
+          val path = Path.explode(Isabelle_System.getenv_strict(s))
+          if (path.elems.exists(_.isInstanceOf[Path.Variable]))
+            error ("Illegal path variable nesting: " + s + "=" + path.toString)
+          else path.elems
         case x => List(x)
       }