| author | wenzelm |
| Thu, 16 Oct 1997 14:46:55 +0200 | |
| changeset 3899 | 41a4abfa60fe |
| parent 3898 | f6bf42312e9e |
| child 3900 | e30bd27a4910 |
| src/Pure/sign.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/sign.ML Thu Oct 16 14:14:01 1997 +0200 +++ b/src/Pure/sign.ML Thu Oct 16 14:46:55 1997 +0200 @@ -817,7 +817,8 @@ fun print_data (Sg {data, ...}) kind = Data.print data kind; (*prepare extension*) -val prep_ext = map_data Data.prep_ext; +fun prep_ext sg = + map_data Data.prep_ext sg |> add_path "/";