# HG changeset patch
# User wenzelm
# Date 1461606099 -7200
# Node ID df83a961d3a82880fafc16ef6a304873507e677d
# Parent  741263be960ee68d43e85aa7d008c707374ad3ab
old 'def' is legacy;

diff -r 741263be960e -r df83a961d3a8 NEWS
--- a/NEWS	Mon Apr 25 17:37:36 2016 +0200
+++ b/NEWS	Mon Apr 25 19:41:39 2016 +0200
@@ -61,7 +61,8 @@
 
 * Command 'define' introduces a local (non-polymorphic) definition, with
 optional abstraction over local parameters. The syntax resembles
-'obtain' and fits better into the Isar language than old 'def'.
+'definition' and 'obtain'. It fits better into the Isar language than
+old 'def', which is now a legacy feature.
 
 * Command '\<proof>' is an alias for 'sorry', with different
 typesetting. E.g. to produce proof holes in examples and documentation.
diff -r 741263be960e -r df83a961d3a8 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Apr 25 17:37:36 2016 +0200
+++ b/src/Pure/Pure.thy	Mon Apr 25 19:41:39 2016 +0200
@@ -749,7 +749,8 @@
       (Parse_Spec.opt_thm_name ":" --
         ((Parse.binding -- Parse.opt_mixfix) --
           ((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp)))
-    >> (Toplevel.proof o Proof.def_cmd));
+    >> (fn args => Toplevel.proof (fn state =>
+        (legacy_feature "Old 'def' command -- use 'define' instead"; Proof.def_cmd args state))));
 
 val _ =
   Outer_Syntax.command @{command_keyword consider} "state cases rule"