# HG changeset patch
# User wenzelm
# Date 877006015 -7200
# Node ID 41a4abfa60fe5a06f1a4e567757ac56247328c6f
# Parent  f6bf42312e9e70727be5551f102dc5d15e454d99
fixed prep_ext;

diff -r f6bf42312e9e -r 41a4abfa60fe src/Pure/sign.ML
--- 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 "/";