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 *)