# HG changeset patch
# User wenzelm
# Date 1159720173 -7200
# Node ID bc3a2b9b996004160d8c51414d200b71b24c2e98
# Parent  379ce56e5dc2110028cb74030b733af9f129a578
reverted to revision 1.28;

diff -r 379ce56e5dc2 -r bc3a2b9b9960 src/Pure/mk
--- a/src/Pure/mk	Sun Oct 01 18:29:32 2006 +0200
+++ b/src/Pure/mk	Sun Oct 01 18:29:33 2006 +0200
@@ -91,7 +91,6 @@
   "$ISABELLE" $COPY \
     -e "val ml_system = \"$ML_SYSTEM\";" \
     -e "val ml_platform = \"$ML_PLATFORM\";" \
-    -e "val share_data = NONE: ('a -> 'a) option;" \
     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
     -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
   RC="$?"