diff -r 43281cd62cb0 -r e0ce214303c1 lib/scripts/run-polyml-5.5.3
--- a/lib/scripts/run-polyml-5.5.3	Sat Jan 10 20:28:53 2015 +0100
+++ b/lib/scripts/run-polyml-5.5.3	Sat Jan 10 21:22:25 2015 +0100
@@ -50,22 +50,20 @@
 fi
 
 if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = false;'
   MLEXIT=""
 else
   if [ -z "$INFILE" ]; then
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
   else
-    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+    MLEXIT="Session.save \"$OUTFILE\";"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-  MLEXIT="commit();"
 fi
 
 
 ## run it!
 
-MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
+MLTEXT="$INIT $EXIT $MLTEXT"
 
 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
   "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \