src/Pure/Isar/isar_cmd.ML
changeset 62169 a6047f511de7
parent 61266 eb9522a9d997
child 62913 13252110a6fe
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jan 13 16:41:32 2016 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jan 13 16:55:56 2016 +0100
     1.3 @@ -16,7 +16,6 @@
     1.4    val translations: (xstring * string) Syntax.trrule list -> theory -> theory
     1.5    val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
     1.6    val oracle: bstring * Position.range -> Input.source -> theory -> theory
     1.7 -  val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
     1.8    val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
     1.9    val simproc_setup: string * Position.T -> string list -> Input.source ->
    1.10      string list -> local_theory -> local_theory
    1.11 @@ -140,18 +139,6 @@
    1.12    end;
    1.13  
    1.14  
    1.15 -(* old-style defs *)
    1.16 -
    1.17 -fun add_defs ((unchecked, overloaded), args) thy =
    1.18 - (legacy_feature ("Old 'defs' command -- use 'definition' (with 'overloading') instead" ^
    1.19 -    Position.here (Position.thread_data ()));
    1.20 -  thy |>
    1.21 -    (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
    1.22 -      overloaded
    1.23 -      (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute_cmd_global thy) srcs)) args)
    1.24 -  |> snd);
    1.25 -
    1.26 -
    1.27  (* declarations *)
    1.28  
    1.29  fun declaration {syntax, pervasive} source =