--- a/NEWS Sun Jul 01 16:46:28 2018 +0100
+++ b/NEWS Sun Jul 01 19:50:33 2018 +0200
@@ -19,10 +19,8 @@
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
-* Global facts need to be closed: no free variables, no hypotheses, no
-pending sort hypotheses. Rare INCOMPATIBILITY: sort hypotheses can be
-allowed via "declare [[pending_shyps]]" in the global theory context,
-but it should be reset to false afterwards.
+* Global facts need to be closed: no free variables and no hypotheses.
+Rare INCOMPATIBILITY.
* Marginal comments need to be written exclusively in the new-style form
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
--- a/src/Doc/Implementation/Logic.thy Sun Jul 01 16:46:28 2018 +0100
+++ b/src/Doc/Implementation/Logic.thy Sun Jul 01 19:50:33 2018 +0200
@@ -862,13 +862,9 @@
class empty =
assumes bad: "\<And>(x::'a) y. x \<noteq> y"
-declare [[pending_shyps]]
-
theorem (in empty) false: False
using bad by blast
-declare [[pending_shyps = false]]
-
ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
text \<open>
--- a/src/Pure/Isar/attrib.ML Sun Jul 01 16:46:28 2018 +0100
+++ b/src/Pure/Isar/attrib.ML Sun Jul 01 19:50:33 2018 +0200
@@ -591,7 +591,6 @@
register_config ML_Options.exception_trace_raw #>
register_config ML_Options.exception_debugger_raw #>
register_config ML_Options.debugger_raw #>
- register_config Global_Theory.pending_shyps_raw #>
register_config Proof_Context.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
register_config Goal_Display.show_main_goal_raw #>
--- a/src/Pure/Tools/dump.scala Sun Jul 01 16:46:28 2018 +0100
+++ b/src/Pure/Tools/dump.scala Sun Jul 01 19:50:33 2018 +0200
@@ -132,7 +132,15 @@
aspects.foreach(_.operation(aspect_args))
}
- session_result
+ if (theories_result.ok) session_result
+ else {
+ for {
+ (name, status) <- theories_result.nodes if !status.ok
+ (tree, pos) <- theories_result.snapshot(name).messages if Protocol.is_error(tree)
+ } progress.echo_error_message(XML.content(Pretty.formatted(List(tree))))
+
+ session_result.copy(rc = session_result.rc max 1)
+ }
}
--- a/src/Pure/global_theory.ML Sun Jul 01 16:46:28 2018 +0100
+++ b/src/Pure/global_theory.ML Sun Jul 01 19:50:33 2018 +0200
@@ -24,8 +24,6 @@
val name_thm: bool -> bool -> string -> thm -> thm
val name_thms: bool -> bool -> string -> thm list -> thm list
val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
- val pending_shyps_raw: Config.raw
- val pending_shyps: bool Config.T
val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
val store_thm: binding * thm -> theory -> thm * theory
val store_thm_open: binding * thm -> theory -> thm * theory
@@ -130,9 +128,6 @@
fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
-val pending_shyps_raw = Config.declare ("pending_shyps", \<^here>) (K (Config.Bool false));
-val pending_shyps = Config.bool pending_shyps_raw;
-
fun add_facts (b, fact) thy =
let
val full_name = Sign.full_name thy b;
@@ -148,8 +143,6 @@
val prop = Thm.plain_prop_of thm
handle THM _ =>
thm
- |> not (Config.get_global thy pending_shyps) ?
- Thm.check_shyps (Proof_Context.init_global thy)
|> Thm.check_hyps (Context.Theory thy)
|> Thm.full_prop_of;
in