Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
command 'use' is legacy;
authorwenzelm
Wed, 29 Aug 2012 13:08:51 +0200
changeset 48997 d1dbc87e3211
parent 48996 a8bad1369ada
child 48998 b6dd664fa9bc
command 'use' is legacy;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- 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"
isabelle