src/Pure/General/secure.ML
changeset 24600 5877b88f262c
parent 24058 81aafd465662
child 24663 015a8838e656
     1.1 --- a/src/Pure/General/secure.ML	Sun Sep 16 14:52:34 2007 +0200
     1.2 +++ b/src/Pure/General/secure.ML	Sun Sep 16 14:55:48 2007 +0200
     1.3 @@ -37,8 +37,8 @@
     1.4  
     1.5  fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
     1.6  
     1.7 -val orig_use_text = use_text;
     1.8 -val orig_use_file = use_file;
     1.9 +fun orig_use_text x = use_text ML_Parse.fix_ints x;
    1.10 +fun orig_use_file x = use_file ML_Parse.fix_ints x;
    1.11  
    1.12  fun use_text name pr verbose txt = NAMED_CRITICAL "ML" (fn () =>
    1.13    (secure_mltext (); orig_use_text name pr verbose txt));