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