discontinued old 'def' command;

--- a/NEWS	Sat Dec 02 16:50:53 2017 +0000
+++ b/NEWS	Sun Dec 03 13:22:09 2017 +0100
@@ -9,6 +9,10 @@
 
 *** General ***
 
+* The old 'def' command has been discontinued (legacy since
+Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
+object-logic equality or equivalence.
+
 * Session-qualified theory names are mandatory: it is no longer possible
 to refer to unqualified theories from the parent session.
 INCOMPATIBILITY for old developments that have not been updated to

--- a/src/Doc/Isar_Ref/Proof.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/Doc/Isar_Ref/Proof.thy	Sun Dec 03 13:22:09 2017 +0100
@@ -128,7 +128,6 @@
     @{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     @{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     @{command_def "define"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
-    @{command_def "def"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
   \end{matharray}
 
   The logical proof context consists of fixed variables and assumptions. The
@@ -169,11 +168,6 @@
     ;
     @@{command define} @{syntax vars} @'where'
       (@{syntax props} + @'and') @{syntax for_fixes}
-    ;
-    @@{command def} (def + @'and')
-    ;
-    def: @{syntax thmdecl}? \<newline>
-      @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
   \<close>}
 
   \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary,
@@ -207,9 +201,6 @@
   \<^medskip>
   It is also possible to abstract over local parameters as follows: \<^theory_text>\<open>define f
   :: "'a \<Rightarrow> 'b" where "f x = t" for x :: 'a\<close>.
-
-  \<^descr> \<^theory_text>\<open>def x \<equiv> t\<close> introduces a local (non-polymorphic) definition. This is an
-  old form of \<^theory_text>\<open>define x where "x = t"\<close>.
 \<close>
 
 

--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sun Dec 03 13:22:09 2017 +0100
@@ -726,7 +726,7 @@
 
 end
 
-sublocale lgrp < "def"?: dgrp
+sublocale lgrp < def?: dgrp
   rewrites one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
 proof -
   show "dgrp(prod)" by unfold_locales

--- a/src/Pure/Isar/proof.ML	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/Pure/Isar/proof.ML	Sun Dec 03 13:22:09 2017 +0100
@@ -68,8 +68,6 @@
   val presume_cmd: (binding * string option * mixfix) list ->
     (string * string list) list list -> (Attrib.binding * (string * string list) list) list ->
     state -> state
-  val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
-  val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
@@ -679,37 +677,6 @@
 end;
 
 
-(* def *)
-
-local
-
-fun gen_def prep_att prep_var prep_binds args state =
-  let
-    val _ = assert_forward state;
-    val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
-    val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
-  in
-    state
-    |> map_context_result (fold_map (fn (x, mx) => prep_var (x, NONE, mx)) raw_vars)
-    |>> map (fn (x, _, mx) => (x, mx))
-    |-> (fn vars =>
-      map_context_result (prep_binds false (map swap raw_rhss))
-      #-> (fn rhss =>
-        let
-          val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
-            ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
-        in map_context_result (Local_Defs.define defs) end))
-    |-> (set_facts o map (#2 o #2))
-  end;
-
-in
-
-val def = gen_def (K I) Proof_Context.cert_var Proof_Context.match_bind;
-val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_var Proof_Context.match_bind_cmd;
-
-end;
-
-
 
 (** facts **)
 

--- a/src/Pure/Pure.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/Pure/Pure.thy	Sun Dec 03 13:22:09 2017 +0100
@@ -55,7 +55,7 @@
   and "note" :: prf_decl % "proof"
   and "supply" :: prf_script % "proof"
   and "using" "unfolding" :: prf_decl % "proof"
-  and "fix" "assume" "presume" "define" "def" :: prf_asm % "proof"
+  and "fix" "assume" "presume" "define" :: prf_asm % "proof"
   and "consider" :: prf_goal % "proof"
   and "obtain" :: prf_asm_goal % "proof"
   and "guess" :: prf_script_asm_goal % "proof"
@@ -807,15 +807,6 @@
       >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
 
 val _ =
-  Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
-    (Parse.and_list1
-      (Parse_Spec.opt_thm_name ":" --
-        ((Parse.binding -- Parse.opt_mixfix) --
-          ((@{keyword \<equiv>} || @{keyword ==}) |-- Parse.!!! Parse.termp)))
-    >> (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"
     (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));