src/Pure/General/path.ML
changeset 41944 b97091ae583a
parent 40627 becf5d5187cc
child 43593 11140987d415
--- a/src/Pure/General/path.ML	Sun Mar 13 15:16:37 2011 +0100
+++ b/src/Pure/General/path.ML	Sun Mar 13 16:01:00 2011 +0100
@@ -20,6 +20,7 @@
   val append: T -> T -> T
   val appends: T list -> T
   val make: string list -> T
+  val print: T -> string
   val implode: T -> string
   val explode: string -> T
   val dir: T -> T
@@ -119,6 +120,8 @@
 
 end;
 
+val print = quote o implode_path;
+
 
 (* explode *)