--- a/src/Pure/Isar/isar_syn.ML Wed Feb 27 16:27:44 2013 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Feb 27 17:32:17 2013 +0100
@@ -270,13 +270,6 @@
(* use ML text *)
val _ =
- Outer_Syntax.command @{command_spec "use"} "ML text from file"
- (Parse.path >> (fn name =>
- Toplevel.generic_theory (fn gthy =>
- (legacy_feature "Old 'use' command -- use 'ML_file' instead";
- Thy_Load.exec_ml (Path.explode name) gthy))));
-
-val _ =
Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
(Parse.ML_source >> (fn (txt, pos) =>
Toplevel.generic_theory