diff -r 6719b465198b -r 4b08766bc9d1 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Mon Dec 16 09:58:16 1996 +0100
+++ b/lib/scripts/run-polyml	Mon Dec 16 09:59:18 1996 +0100
@@ -17,9 +17,8 @@
 }
 
 
-## locations and settings
+## Poly/ML programs
 
-ML_DBASE=$ML_HOME/ML_dbase
 POLY=$ML_HOME/poly
 DISCGARB=$ML_HOME/discgarb
 
@@ -35,7 +34,7 @@
 MLINIT=""
 
 if [ -z "$INFILE" ]; then
-  INFILE="$ML_DBASE"
+  INFILE="$ML_HOME/ML_dbase"
   MLINIT="val use = PolyML.use; val exit = PolyML.exit; fun init_database () = ();"
 fi
 
@@ -60,22 +59,19 @@
 ## run it!
 
 START_POLY="$POLY $ML_OPTIONS $DB"
-DB_INFO=$(ls -l $DB)
+DB_INFO=$(ls -l "$DB")
 
 [ -n "$MLINIT" ] && MLTEXT="$MLINIT $MLTEXT"
 
 if [ -n "$TERMINATE" ]; then
   echo "$MLTEXT" | $START_POLY
   RC=$?
-elif [ -z "$MLTEXT" ]; then
-  $START_POLY
-  RC=$?
 else
-  { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat } | $START_POLY
+  { echo "$MLTEXT"; $ISABELLE_HOME/lib/Tools/symbolinput } | $START_POLY
   RC=$?
 fi
 
-NEW_DB_INFO=$(ls -l $DB)
+NEW_DB_INFO=$(ls -l "$DB")
 [ $RC -eq 0 -a -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
 
 exit $RC