src/Pure/Thy/present.ML
changeset 33955 fff6f11b1f09
parent 33682 0c5d1485dea7
child 33957 e9afca2118d4
--- a/src/Pure/Thy/present.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Thy/present.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -285,7 +285,7 @@
     (browser_info := empty_browser_info; session_info := NONE)
   else
     let
-      val parent_name = name_of_session (Library.take (length path - 1, path));
+      val parent_name = name_of_session ((uncurry take) (length path - 1, path));
       val session_name = name_of_session path;
       val sess_prefix = Path.make path;
       val html_prefix = Path.append (Path.expand output_path) sess_prefix;