# HG changeset patch
# User wenzelm
# Date 1361982737 -3600
# Node ID 71fc3776c4537c445f7c90048c8b09e75ec3354b
# Parent  0850d43cb355df7e57fd0d6ae0011058ef38634c
discontinued redundant 'use' command;

diff -r 0850d43cb355 -r 71fc3776c453 NEWS
--- a/NEWS	Wed Feb 27 16:27:44 2013 +0100
+++ b/NEWS	Wed Feb 27 17:32:17 2013 +0100
@@ -10,6 +10,9 @@
 commands like 'ML_file' work without separate declaration of file
 dependencies.  Minor INCOMPATIBILITY.
 
+* Discontinued redundant 'use' command, which was superseded by
+'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.
+
 
 *** HOL ***
 
diff -r 0850d43cb355 -r 71fc3776c453 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Wed Feb 27 16:27:44 2013 +0100
+++ b/etc/isar-keywords-ZF.el	Wed Feb 27 17:32:17 2013 +0100
@@ -200,7 +200,6 @@
     "undos_proof"
     "unfolding"
     "unused_thms"
-    "use"
     "use_thy"
     "using"
     "welcome"
@@ -407,8 +406,7 @@
     "type_notation"
     "type_synonym"
     "typed_print_translation"
-    "typedecl"
-    "use"))
+    "typedecl"))
 
 (defconst isar-keywords-theory-script
   '("inductive_cases"))
diff -r 0850d43cb355 -r 71fc3776c453 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Feb 27 16:27:44 2013 +0100
+++ b/etc/isar-keywords.el	Wed Feb 27 17:32:17 2013 +0100
@@ -288,7 +288,6 @@
     "undos_proof"
     "unfolding"
     "unused_thms"
-    "use"
     "use_thy"
     "using"
     "value"
@@ -573,8 +572,7 @@
     "type_notation"
     "type_synonym"
     "typed_print_translation"
-    "typedecl"
-    "use"))
+    "typedecl"))
 
 (defconst isar-keywords-theory-script
   '("inductive_cases"
diff -r 0850d43cb355 -r 71fc3776c453 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Wed Feb 27 16:27:44 2013 +0100
+++ b/src/Doc/IsarImplementation/ML.thy	Wed Feb 27 17:32:17 2013 +0100
@@ -540,7 +540,7 @@
 
 text {* The primary Isar source language provides facilities to ``open
   a window'' to the underlying ML compiler.  Especially see the Isar
-  commands @{command_ref "use"} and @{command_ref "ML"}: both work the
+  commands @{command_ref "ML_file"} and @{command_ref "ML"}: both work the
   same way, only the source text is provided via a file vs.\ inlined,
   respectively.  Apart from embedding ML into the main theory
   definition like that, there are many more commands that refer to ML
diff -r 0850d43cb355 -r 71fc3776c453 src/Pure/Isar/isar_syn.ML
--- 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
diff -r 0850d43cb355 -r 71fc3776c453 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Feb 27 16:27:44 2013 +0100
+++ b/src/Pure/Pure.thy	Wed Feb 27 17:32:17 2013 +0100
@@ -29,7 +29,7 @@
     "abbreviation" "type_notation" "no_type_notation" "notation"
     "no_notation" "axiomatization" "theorems" "lemmas" "declare"
     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
-  and "use" "ML" :: thy_decl % "ML"
+  and "ML" :: thy_decl % "ML"
   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
   and "ML_val" "ML_command" :: diag % "ML"
   and "setup" "local_setup" "attribute_setup" "method_setup"