Admin/makebin

 with_path ".." use_thy "HOL4Syntax";
 use_thy "HOL4Prob";
 use_thy "HOL4";
 EOF
 
+perl -pi \
+  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \
+  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \
+  etc/settings
+
 if [ -n "$DO_LIBRARY" ]; then
-  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-i true -d pdf -V outline=/proof,/ML":' \
-    etc/settings
-else
-  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 2":' \
+  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1 -i true -d pdf -V outline=/proof,/ML":;' \
     etc/settings
 fi
 
 ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \

   mkdir browser_info
 elif [ -n "$DO_LIBRARY" ]; then
   ./build -bait
 else
   ./build -b -m HOL-Complex HOL
+  ./build -b -m HOL4 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