# HG changeset patch
# User wenzelm
# Date 1294936252 -3600
# Node ID 0112f14d75ec2a89bdd49ccaf0ec59c6b2aae8f2
# Parent  f36cb6f233bdf1de6dd7d961ac600f6b926885cc
clarified split_thy_path;

diff -r f36cb6f233bd -r 0112f14d75ec src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Thu Jan 13 17:27:52 2011 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Jan 13 17:30:52 2011 +0100
@@ -30,7 +30,7 @@
   /* file name */
 
   val Thy_Path1 = new Regex("([^/]*)\\.thy")
-  val Thy_Path2 = new Regex("(.*/)([^/]*)\\.thy")
+  val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
 
   def split_thy_path(path: String): Option[(String, String)] =
     path match {