# HG changeset patch
# User wenzelm
# Date 1530467433 -7200
# Node ID a059271424d0ebcb808d607fff6a3c9d5bb23422
# Parent  fcffdcb8f5067c3e75a909f4840c0e61b9375fc8# Parent  7aae213d9e6946186b2e420582369fe9ae16721e
merged

diff -r fcffdcb8f506 -r a059271424d0 NEWS
--- 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
diff -r fcffdcb8f506 -r a059271424d0 src/Doc/Implementation/Logic.thy
--- 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>
diff -r fcffdcb8f506 -r a059271424d0 src/Pure/Isar/attrib.ML
--- 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 #>
diff -r fcffdcb8f506 -r a059271424d0 src/Pure/Tools/dump.scala
--- 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)
+    }
   }
 
 
diff -r fcffdcb8f506 -r a059271424d0 src/Pure/global_theory.ML
--- 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