changeset 56434 | 7acc933bd7cc |
parent 44200 | ce0112e26b3b |
child 58842 | 22b87ab47d3b |
--- a/src/Pure/General/secure.ML Sun Apr 06 14:30:26 2014 +0200 +++ b/src/Pure/General/secure.ML Sun Apr 06 15:19:22 2014 +0200 @@ -58,15 +58,3 @@ end; -(*override previous toplevel bindings!*) -val use_text = Secure.use_text; -val use_file = Secure.use_file; - -fun use s = - Position.setmp_thread_data (Position.file_only s) - (fn () => - Secure.use_file ML_Parse.global_context true s - handle ERROR msg => (writeln msg; error "ML error")) (); - -val toplevel_pp = Secure.toplevel_pp; -