discontinued pending_shyps: too much complication due to lazy facts;
authorwenzelm
Sun Jul 01 12:38:37 2018 +0200 (11 months ago)
changeset 685587aae213d9e69
parent 68557 5a836f1b588c
child 68559 a059271424d0
discontinued pending_shyps: too much complication due to lazy facts;
NEWS
src/Doc/Implementation/Logic.thy
src/Pure/Isar/attrib.ML
src/Pure/global_theory.ML
     1.1 --- a/NEWS	Sun Jul 01 12:37:24 2018 +0200
     1.2 +++ b/NEWS	Sun Jul 01 12:38:37 2018 +0200
     1.3 @@ -19,10 +19,8 @@
     1.4  FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
     1.5  formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
     1.6  
     1.7 -* Global facts need to be closed: no free variables, no hypotheses, no
     1.8 -pending sort hypotheses. Rare INCOMPATIBILITY: sort hypotheses can be
     1.9 -allowed via "declare [[pending_shyps]]" in the global theory context,
    1.10 -but it should be reset to false afterwards.
    1.11 +* Global facts need to be closed: no free variables and no hypotheses.
    1.12 +Rare INCOMPATIBILITY.
    1.13  
    1.14  * Marginal comments need to be written exclusively in the new-style form
    1.15  "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
     2.1 --- a/src/Doc/Implementation/Logic.thy	Sun Jul 01 12:37:24 2018 +0200
     2.2 +++ b/src/Doc/Implementation/Logic.thy	Sun Jul 01 12:38:37 2018 +0200
     2.3 @@ -862,13 +862,9 @@
     2.4  class empty =
     2.5    assumes bad: "\<And>(x::'a) y. x \<noteq> y"
     2.6  
     2.7 -declare [[pending_shyps]]
     2.8 -
     2.9  theorem (in empty) false: False
    2.10    using bad by blast
    2.11  
    2.12 -declare [[pending_shyps = false]]
    2.13 -
    2.14  ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
    2.15  
    2.16  text \<open>
     3.1 --- a/src/Pure/Isar/attrib.ML	Sun Jul 01 12:37:24 2018 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Sun Jul 01 12:38:37 2018 +0200
     3.3 @@ -591,7 +591,6 @@
     3.4    register_config ML_Options.exception_trace_raw #>
     3.5    register_config ML_Options.exception_debugger_raw #>
     3.6    register_config ML_Options.debugger_raw #>
     3.7 -  register_config Global_Theory.pending_shyps_raw #>
     3.8    register_config Proof_Context.show_abbrevs_raw #>
     3.9    register_config Goal_Display.goals_limit_raw #>
    3.10    register_config Goal_Display.show_main_goal_raw #>
     4.1 --- a/src/Pure/global_theory.ML	Sun Jul 01 12:37:24 2018 +0200
     4.2 +++ b/src/Pure/global_theory.ML	Sun Jul 01 12:38:37 2018 +0200
     4.3 @@ -24,8 +24,6 @@
     4.4    val name_thm: bool -> bool -> string -> thm -> thm
     4.5    val name_thms: bool -> bool -> string -> thm list -> thm list
     4.6    val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
     4.7 -  val pending_shyps_raw: Config.raw
     4.8 -  val pending_shyps: bool Config.T
     4.9    val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
    4.10    val store_thm: binding * thm -> theory -> thm * theory
    4.11    val store_thm_open: binding * thm -> theory -> thm * theory
    4.12 @@ -130,9 +128,6 @@
    4.13  
    4.14  fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
    4.15  
    4.16 -val pending_shyps_raw = Config.declare ("pending_shyps", \<^here>) (K (Config.Bool false));
    4.17 -val pending_shyps = Config.bool pending_shyps_raw;
    4.18 -
    4.19  fun add_facts (b, fact) thy =
    4.20    let
    4.21      val full_name = Sign.full_name thy b;
    4.22 @@ -148,8 +143,6 @@
    4.23            val prop = Thm.plain_prop_of thm
    4.24              handle THM _ =>
    4.25                thm
    4.26 -              |> not (Config.get_global thy pending_shyps) ?
    4.27 -                  Thm.check_shyps (Proof_Context.init_global thy)
    4.28                |> Thm.check_hyps (Context.Theory thy)
    4.29                |> Thm.full_prop_of;
    4.30          in