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