# HG changeset patch
# User wenzelm
# Date 1309384860 -7200
# Node ID e0ee016fc4fdd62ef27189981736dc7165b35edf
# Parent  826ddd91ae2b6e59e9a043b90ed58df82b60a370
proper Path.print;

diff -r 826ddd91ae2b -r e0ee016fc4fd src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed Jun 29 23:43:48 2011 +0200
+++ b/src/Pure/General/path.ML	Thu Jun 30 00:01:00 2011 +0200
@@ -163,7 +163,7 @@
 (* base element *)
 
 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)
-  | split_path _ path = error ("Cannot split path into dir/base: " ^ quote (implode_path path));
+  | split_path _ path = error ("Cannot split path into dir/base: " ^ print path);
 
 val dir = split_path #1;
 val base = split_path (fn (_, s) => Path [Basic s]);