src/Pure/General/secure.ML
changeset 24663 015a8838e656
parent 24600 5877b88f262c
child 24858 a3a81e73f552
equal deleted inserted replaced
24662:f79f6061525c 24663:015a8838e656
    68 end;
    68 end;
    69 
    69 
    70 (*override previous toplevel bindings!*)
    70 (*override previous toplevel bindings!*)
    71 val use_text = Secure.use_text;
    71 val use_text = Secure.use_text;
    72 val use_file = Secure.use_file;
    72 val use_file = Secure.use_file;
    73 val use = Secure.use;
    73 fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
    74 val execute = Secure.execute;
    74 val execute = Secure.execute;
    75 val system = Secure.system;
    75 val system = Secure.system;