# HG changeset patch
# User wenzelm
# Date 1530441517 -7200
# Node ID 7aae213d9e6946186b2e420582369fe9ae16721e
# Parent  5a836f1b588c7e75854a1ff23e7a4879065cea9d
discontinued pending_shyps: too much complication due to lazy facts;

diff -r 5a836f1b588c -r 7aae213d9e69 NEWS
--- a/NEWS	Sun Jul 01 12:37:24 2018 +0200
+++ b/NEWS	Sun Jul 01 12:38:37 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 5a836f1b588c -r 7aae213d9e69 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sun Jul 01 12:37:24 2018 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sun Jul 01 12:38:37 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 5a836f1b588c -r 7aae213d9e69 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Jul 01 12:37:24 2018 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Jul 01 12:38:37 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 5a836f1b588c -r 7aae213d9e69 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sun Jul 01 12:37:24 2018 +0200
+++ b/src/Pure/global_theory.ML	Sun Jul 01 12:38:37 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