--- 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 ***
--- 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 =
--- 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 _ =
--- 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
--- 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;