1.1 --- a/Admin/makebin	Wed May 30 21:09:18 2007 +0200
     1.2 +++ b/Admin/makebin	Wed May 30 23:31:57 2007 +0200
     1.3 @@ -91,16 +91,6 @@
     1.4  "$TAR" xzf "$ARCHIVE_FULL"
     1.5  cd "$ISABELLE_NAME"
     1.6  
     1.7 -# FIXME: ugly hack to get proper HOL4 image
     1.8 -# needs HOL4 proof terms installed in ~/isabelle/proofs
     1.9 -# desperately needs fix for next release!
    1.10 -cat > src/HOL/Import/HOL/ROOT.ML <<EOF
    1.11 -with_path ".." use_thy "HOL4Compat";
    1.12 -with_path ".." use_thy "HOL4Syntax";
    1.13 -use_thy "HOL4Prob";
    1.14 -use_thy "HOL4";
    1.15 -EOF
    1.16 -
    1.17  perl -pi \
    1.18    -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \
    1.19    -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \
    1.20 @@ -124,8 +114,6 @@
    1.21    touch "heaps/$COMPILER/log/HOL.gz"
    1.22    touch "heaps/$COMPILER/HOL-Complex"
    1.23    touch "heaps/$COMPILER/log/HOL-Complex.gz"
    1.24 -  touch "heaps/$COMPILER/HOL4"
    1.25 -  touch "heaps/$COMPILER/log/HOL4.gz"
    1.26    touch "heaps/$COMPILER/ZF"
    1.27    touch "heaps/$COMPILER/log/ZF.gz"
    1.28    mkdir browser_info
    1.29 @@ -133,7 +121,6 @@
    1.30    ./build -bait
    1.31  else
    1.32    ./build -b -m HOL-Complex HOL
    1.33 -  ./build -b -m HOL4 HOL
    1.34    ./build -b ZF
    1.35    rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
    1.36  fi
    1.37 @@ -151,7 +138,7 @@
    1.38      gzip -f "${ISABELLE_NAME}_library.tar"
    1.39      cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
    1.40  else
    1.41 -  for IMG in HOL HOL-Complex HOL4 ZF
    1.42 +  for IMG in HOL HOL-Complex ZF
    1.43    do
    1.44      "$TAR" cf "${IMG}_$PLATFORM.tar" \
    1.45        "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \