Admin/makebin

 
 cd "$TMP"
 "$TAR" xzf "$ARCHIVE_FULL"
 cd "$ISABELLE_NAME"
 
+# FIXME: ugly hack to get proper HOL4 image
+# needs HOL4 proof terms installed in ~/isabelle/proofs
+# desperately needs fix for next release!
+cat > src/HOL/Import/HOL/ROOT.ML <<EOF
+with_path ".." use_thy "HOL4Compat";
+with_path ".." use_thy "HOL4Syntax";
+use_thy "HOL4Prob";
+use_thy "HOL4";
+EOF
+
 if [ -n "$DO_LIBRARY" ]; then
   perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-i true -d pdf"/' \
     etc/settings
 else
   perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 2"/' \

   mkdir -p "heaps/$COMPILER/log"
   touch "heaps/$COMPILER/HOL"
   touch "heaps/$COMPILER/log/HOL.gz"
   touch "heaps/$COMPILER/HOL-Complex"
   touch "heaps/$COMPILER/log/HOL-Complex.gz"
+  touch "heaps/$COMPILER/HOL4"
+  touch "heaps/$COMPILER/log/HOL4.gz"
   touch "heaps/$COMPILER/ZF"
   touch "heaps/$COMPILER/log/ZF.gz"
   mkdir browser_info
 elif [ -n "$DO_LIBRARY" ]; then
   ./build -bait
 else
   ./build -b -m HOL-Complex HOL
   ./build -b ZF
+  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 1"/' \
+    etc/settings
+  ./build -b -m HOL4 HOL
   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
 fi
 
 
 # prepare result

 if [ -n "$DO_LIBRARY" ]; then
   "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
     gzip -f "${ISABELLE_NAME}_library.tar"
     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
 else
-  for IMG in HOL HOL-Complex ZF
+  for IMG in HOL HOL-Complex HOL4 ZF
   do
     "$TAR" cf "${IMG}_$PLATFORM.tar" \
       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
     gzip -f "${IMG}_$PLATFORM.tar"