removed old 'defs' command;
authorwenzelm
Wed Jan 13 16:55:56 2016 +0100 (2016-01-13 ago)
changeset 62169a6047f511de7
parent 62168 e97452d79102
child 62170 b61c55e4b4b9
removed old 'defs' command;
NEWS
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Pure/global_theory.ML
     1.1 --- a/NEWS	Wed Jan 13 16:41:32 2016 +0100
     1.2 +++ b/NEWS	Wed Jan 13 16:55:56 2016 +0100
     1.3 @@ -53,6 +53,10 @@
     1.4  * Toplevel theorem statement 'proposition' is another alias for
     1.5  'theorem'.
     1.6  
     1.7 +* The old 'defs' command has been removed (legacy since Isabelle2014).
     1.8 +INCOMPATIBILITY, use regular 'definition' instead. Overloaded and/or
     1.9 +deferred definitions require a surrounding 'overloading' block.
    1.10 +
    1.11  
    1.12  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.13  
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jan 13 16:41:32 2016 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jan 13 16:55:56 2016 +0100
     2.3 @@ -16,7 +16,6 @@
     2.4    val translations: (xstring * string) Syntax.trrule list -> theory -> theory
     2.5    val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
     2.6    val oracle: bstring * Position.range -> Input.source -> theory -> theory
     2.7 -  val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
     2.8    val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
     2.9    val simproc_setup: string * Position.T -> string list -> Input.source ->
    2.10      string list -> local_theory -> local_theory
    2.11 @@ -140,18 +139,6 @@
    2.12    end;
    2.13  
    2.14  
    2.15 -(* old-style defs *)
    2.16 -
    2.17 -fun add_defs ((unchecked, overloaded), args) thy =
    2.18 - (legacy_feature ("Old 'defs' command -- use 'definition' (with 'overloading') instead" ^
    2.19 -    Position.here (Position.thread_data ()));
    2.20 -  thy |>
    2.21 -    (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
    2.22 -      overloaded
    2.23 -      (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute_cmd_global thy) srcs)) args)
    2.24 -  |> snd);
    2.25 -
    2.26 -
    2.27  (* declarations *)
    2.28  
    2.29  fun declaration {syntax, pervasive} source =
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jan 13 16:41:32 2016 +0100
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 13 16:55:56 2016 +0100
     3.3 @@ -90,21 +90,6 @@
     3.4      (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
     3.5  
     3.6  
     3.7 -(* axioms and definitions *)
     3.8 -
     3.9 -val opt_unchecked_overloaded =
    3.10 -  Scan.optional (@{keyword "("} |-- Parse.!!!
    3.11 -    (((@{keyword "unchecked"} >> K true) --
    3.12 -        Scan.optional (@{keyword "overloaded"} >> K true) false ||
    3.13 -      @{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false);
    3.14 -
    3.15 -val _ =
    3.16 -  Outer_Syntax.command @{command_keyword defs} "define constants"
    3.17 -    (opt_unchecked_overloaded --
    3.18 -      Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
    3.19 -      >> (Toplevel.theory o Isar_Cmd.add_defs));
    3.20 -
    3.21 -
    3.22  (* constant definitions and abbreviations *)
    3.23  
    3.24  val _ =
     4.1 --- a/src/Pure/Pure.thy	Wed Jan 13 16:41:32 2016 +0100
     4.2 +++ b/src/Pure/Pure.thy	Wed Jan 13 16:55:56 2016 +0100
     4.3 @@ -17,7 +17,7 @@
     4.4    and "text_raw" :: document_raw
     4.5    and "default_sort" :: thy_decl == ""
     4.6    and "typedecl" "type_synonym" "nonterminal" "judgment"
     4.7 -    "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
     4.8 +    "consts" "syntax" "no_syntax" "translations" "no_translations"
     4.9      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    4.10      "no_notation" "axiomatization" "lemmas" "declare"
    4.11      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
     5.1 --- a/src/Pure/global_theory.ML	Wed Jan 13 16:41:32 2016 +0100
     5.2 +++ b/src/Pure/global_theory.ML	Wed Jan 13 16:55:56 2016 +0100
     5.3 @@ -39,10 +39,6 @@
     5.4      theory -> thm list * theory
     5.5    val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
     5.6      theory -> thm list * theory
     5.7 -  val add_defs_cmd: bool -> ((binding * string) * attribute list) list ->
     5.8 -    theory -> thm list * theory
     5.9 -  val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list ->
    5.10 -    theory -> thm list * theory
    5.11  end;
    5.12  
    5.13  structure Global_Theory: GLOBAL_THEORY =
    5.14 @@ -197,16 +193,9 @@
    5.15  
    5.16  local
    5.17  
    5.18 -fun no_read _ (_, t) = t;
    5.19 -
    5.20 -fun read ctxt (b, str) =
    5.21 -  Syntax.read_prop ctxt str handle ERROR msg =>
    5.22 -    cat_error msg ("The error(s) above occurred in definition " ^ Binding.print b);
    5.23 -
    5.24 -fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
    5.25 +fun add unchecked overloaded = fold_map (fn ((b, prop), atts) => fn thy =>
    5.26    let
    5.27      val context as (ctxt, _) = Defs.global_context thy;
    5.28 -    val prop = prep ctxt (b, raw_prop);
    5.29      val ((_, def), thy') = Thm.add_def context unchecked overloaded (b, prop) thy;
    5.30      val thm = def
    5.31        |> Thm.forall_intr_frees
    5.32 @@ -216,10 +205,8 @@
    5.33  
    5.34  in
    5.35  
    5.36 -val add_defs = add no_read false;
    5.37 -val add_defs_unchecked = add no_read true;
    5.38 -val add_defs_cmd = add read false;
    5.39 -val add_defs_unchecked_cmd = add read true;
    5.40 +val add_defs = add false;
    5.41 +val add_defs_unchecked = add true;
    5.42  
    5.43  end;
    5.44