diff -r 7b0ecf9a9055 -r 5877b88f262c src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Sun Sep 16 14:52:34 2007 +0200
+++ b/src/Pure/General/secure.ML	Sun Sep 16 14:55:48 2007 +0200
@@ -37,8 +37,8 @@
 
 fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
 
-val orig_use_text = use_text;
-val orig_use_file = use_file;
+fun orig_use_text x = use_text ML_Parse.fix_ints x;
+fun orig_use_file x = use_file ML_Parse.fix_ints x;
 
 fun use_text name pr verbose txt = NAMED_CRITICAL "ML" (fn () =>
   (secure_mltext (); orig_use_text name pr verbose txt));