# HG changeset patch
# User wenzelm
# Date 1452700556 -3600
# Node ID a6047f511de7aa2da6e7bf7c2166abac1c25ed57
# Parent  e97452d79102607f82a5ed8624c11498adfc8ec1
removed old 'defs' command;

diff -r e97452d79102 -r a6047f511de7 NEWS
--- a/NEWS	Wed Jan 13 16:41:32 2016 +0100
+++ b/NEWS	Wed Jan 13 16:55:56 2016 +0100
@@ -53,6 +53,10 @@
 * Toplevel theorem statement 'proposition' is another alias for
 'theorem'.
 
+* The old 'defs' command has been removed (legacy since Isabelle2014).
+INCOMPATIBILITY, use regular 'definition' instead. Overloaded and/or
+deferred definitions require a surrounding 'overloading' block.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r e97452d79102 -r a6047f511de7 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Jan 13 16:41:32 2016 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jan 13 16:55:56 2016 +0100
@@ -16,7 +16,6 @@
   val translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val oracle: bstring * Position.range -> Input.source -> theory -> theory
-  val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
   val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
   val simproc_setup: string * Position.T -> string list -> Input.source ->
     string list -> local_theory -> local_theory
@@ -140,18 +139,6 @@
   end;
 
 
-(* old-style defs *)
-
-fun add_defs ((unchecked, overloaded), args) thy =
- (legacy_feature ("Old 'defs' command -- use 'definition' (with 'overloading') instead" ^
-    Position.here (Position.thread_data ()));
-  thy |>
-    (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
-      overloaded
-      (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute_cmd_global thy) srcs)) args)
-  |> snd);
-
-
 (* declarations *)
 
 fun declaration {syntax, pervasive} source =
diff -r e97452d79102 -r a6047f511de7 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jan 13 16:41:32 2016 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 13 16:55:56 2016 +0100
@@ -90,21 +90,6 @@
     (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
 
 
-(* axioms and definitions *)
-
-val opt_unchecked_overloaded =
-  Scan.optional (@{keyword "("} |-- Parse.!!!
-    (((@{keyword "unchecked"} >> K true) --
-        Scan.optional (@{keyword "overloaded"} >> K true) false ||
-      @{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false);
-
-val _ =
-  Outer_Syntax.command @{command_keyword defs} "define constants"
-    (opt_unchecked_overloaded --
-      Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
-      >> (Toplevel.theory o Isar_Cmd.add_defs));
-
-
 (* constant definitions and abbreviations *)
 
 val _ =
diff -r e97452d79102 -r a6047f511de7 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Jan 13 16:41:32 2016 +0100
+++ b/src/Pure/Pure.thy	Wed Jan 13 16:55:56 2016 +0100
@@ -17,7 +17,7 @@
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl == ""
   and "typedecl" "type_synonym" "nonterminal" "judgment"
-    "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
+    "consts" "syntax" "no_syntax" "translations" "no_translations"
     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     "no_notation" "axiomatization" "lemmas" "declare"
     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
diff -r e97452d79102 -r a6047f511de7 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Wed Jan 13 16:41:32 2016 +0100
+++ b/src/Pure/global_theory.ML	Wed Jan 13 16:55:56 2016 +0100
@@ -39,10 +39,6 @@
     theory -> thm list * theory
   val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
     theory -> thm list * theory
-  val add_defs_cmd: bool -> ((binding * string) * attribute list) list ->
-    theory -> thm list * theory
-  val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list ->
-    theory -> thm list * theory
 end;
 
 structure Global_Theory: GLOBAL_THEORY =
@@ -197,16 +193,9 @@
 
 local
 
-fun no_read _ (_, t) = t;
-
-fun read ctxt (b, str) =
-  Syntax.read_prop ctxt str handle ERROR msg =>
-    cat_error msg ("The error(s) above occurred in definition " ^ Binding.print b);
-
-fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
+fun add unchecked overloaded = fold_map (fn ((b, prop), atts) => fn thy =>
   let
     val context as (ctxt, _) = Defs.global_context thy;
-    val prop = prep ctxt (b, raw_prop);
     val ((_, def), thy') = Thm.add_def context unchecked overloaded (b, prop) thy;
     val thm = def
       |> Thm.forall_intr_frees
@@ -216,10 +205,8 @@
 
 in
 
-val add_defs = add no_read false;
-val add_defs_unchecked = add no_read true;
-val add_defs_cmd = add read false;
-val add_defs_unchecked_cmd = add read true;
+val add_defs = add false;
+val add_defs_unchecked = add true;
 
 end;