merged
authorwenzelm
Sun Jul 01 19:50:33 2018 +0200 (9 months ago)
changeset 68559a059271424d0
parent 68556 fcffdcb8f506
parent 68558 7aae213d9e69
child 68560 ad079be4f21c
merged
     1.1 --- a/NEWS	Sun Jul 01 16:46:28 2018 +0100
     1.2 +++ b/NEWS	Sun Jul 01 19:50:33 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 16:46:28 2018 +0100
     2.2 +++ b/src/Doc/Implementation/Logic.thy	Sun Jul 01 19:50:33 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 16:46:28 2018 +0100
     3.2 +++ b/src/Pure/Isar/attrib.ML	Sun Jul 01 19:50:33 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/Tools/dump.scala	Sun Jul 01 16:46:28 2018 +0100
     4.2 +++ b/src/Pure/Tools/dump.scala	Sun Jul 01 19:50:33 2018 +0200
     4.3 @@ -132,7 +132,15 @@
     4.4        aspects.foreach(_.operation(aspect_args))
     4.5      }
     4.6  
     4.7 -    session_result
     4.8 +    if (theories_result.ok) session_result
     4.9 +    else {
    4.10 +      for {
    4.11 +        (name, status) <- theories_result.nodes if !status.ok
    4.12 +        (tree, pos) <- theories_result.snapshot(name).messages if Protocol.is_error(tree)
    4.13 +      } progress.echo_error_message(XML.content(Pretty.formatted(List(tree))))
    4.14 +
    4.15 +      session_result.copy(rc = session_result.rc max 1)
    4.16 +    }
    4.17    }
    4.18  
    4.19  
     5.1 --- a/src/Pure/global_theory.ML	Sun Jul 01 16:46:28 2018 +0100
     5.2 +++ b/src/Pure/global_theory.ML	Sun Jul 01 19:50:33 2018 +0200
     5.3 @@ -24,8 +24,6 @@
     5.4    val name_thm: bool -> bool -> string -> thm -> thm
     5.5    val name_thms: bool -> bool -> string -> thm list -> thm list
     5.6    val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
     5.7 -  val pending_shyps_raw: Config.raw
     5.8 -  val pending_shyps: bool Config.T
     5.9    val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
    5.10    val store_thm: binding * thm -> theory -> thm * theory
    5.11    val store_thm_open: binding * thm -> theory -> thm * theory
    5.12 @@ -130,9 +128,6 @@
    5.13  
    5.14  fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
    5.15  
    5.16 -val pending_shyps_raw = Config.declare ("pending_shyps", \<^here>) (K (Config.Bool false));
    5.17 -val pending_shyps = Config.bool pending_shyps_raw;
    5.18 -
    5.19  fun add_facts (b, fact) thy =
    5.20    let
    5.21      val full_name = Sign.full_name thy b;
    5.22 @@ -148,8 +143,6 @@
    5.23            val prop = Thm.plain_prop_of thm
    5.24              handle THM _ =>
    5.25                thm
    5.26 -              |> not (Config.get_global thy pending_shyps) ?
    5.27 -                  Thm.check_shyps (Proof_Context.init_global thy)
    5.28                |> Thm.check_hyps (Context.Theory thy)
    5.29                |> Thm.full_prop_of;
    5.30          in