src/Pure/sign.ML
changeset 3899 41a4abfa60fe
parent 3886 eb0681305d3f
child 3937 988ce6fbf85b
     1.1 --- a/src/Pure/sign.ML	Thu Oct 16 14:14:01 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Oct 16 14:46:55 1997 +0200
     1.3 @@ -817,7 +817,8 @@
     1.4  fun print_data (Sg {data, ...}) kind = Data.print data kind;
     1.5  
     1.6  (*prepare extension*)
     1.7 -val prep_ext = map_data Data.prep_ext;
     1.8 +fun prep_ext sg =
     1.9 +  map_data Data.prep_ext sg |> add_path "/";
    1.10  
    1.11  
    1.12