author | wenzelm |
Thu, 30 Jun 2011 00:01:00 +0200 | |
changeset 43599 | e0ee016fc4fd |
parent 43598 | 826ddd91ae2b |
child 43600 | 4ac04bf9ff89 |
--- 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]);