diff -r db69cb14f7ed -r 7acc933bd7cc src/Pure/General/secure.ML --- 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; -