# HG changeset patch
# User wenzelm
# Date 1346238531 -7200
# Node ID d1dbc87e3211febc433d21e5d722e7cfaa07f0fa
# Parent  a8bad1369adad98ebf06b5cad846ba81d72a4f65
command 'use' is legacy;

diff -r a8bad1369ada -r d1dbc87e3211 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 29 12:55:41 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 29 13:08:51 2012 +0200
@@ -272,7 +272,9 @@
 val _ =
   Outer_Syntax.command @{command_spec "use"} "ML text from file"
     (Parse.path >> (fn name =>
-      Toplevel.generic_theory (fn gthy => Thy_Load.exec_ml (Path.explode name) gthy)));
+      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"