# HG changeset patch
# User wenzelm
# Date 1530280481 -7200
# Node ID 000a0e062529b3de3a6c0dff0e0ddce60c847fa9
# Parent  6740e3611a869cebaac5d98d2915ea5122e9c632
disallow pending hyps;
disallow pending shyps, with option to override the check;
tuned message;

diff -r 6740e3611a86 -r 000a0e062529 NEWS
--- a/NEWS	Fri Jun 29 14:19:52 2018 +0200
+++ b/NEWS	Fri Jun 29 15:54:41 2018 +0200
@@ -19,6 +19,11 @@
 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.
+
 * Marginal comments need to be written exclusively in the new-style form
 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
 supported. INCOMPATIBILITY, use the command-line tool "isabelle
diff -r 6740e3611a86 -r 000a0e062529 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Fri Jun 29 14:19:52 2018 +0200
+++ b/src/Doc/Implementation/Logic.thy	Fri Jun 29 15:54:41 2018 +0200
@@ -862,9 +862,13 @@
 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 6740e3611a86 -r 000a0e062529 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Jun 29 14:19:52 2018 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Jun 29 15:54:41 2018 +0200
@@ -591,6 +591,7 @@
   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 6740e3611a86 -r 000a0e062529 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Jun 29 14:19:52 2018 +0200
+++ b/src/Pure/global_theory.ML	Fri Jun 29 15:54:41 2018 +0200
@@ -24,6 +24,8 @@
   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
@@ -128,16 +130,35 @@
 
 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;
     val pos = Binding.pos_of b;
-    fun err msg =
-      error ("Malformed global fact " ^ quote full_name ^ Position.here pos ^ "\n" ^ msg);
-    fun check thm =
-      ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes (Thm.full_prop_of thm)))
-        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
-    val arg = (b, Lazy.map_finished (tap (List.app check)) fact);
+    fun check fact =
+      fact |> map_index (fn (i, thm) =>
+        let
+          fun err msg =
+            error ("Malformed global fact " ^
+              quote (full_name ^
+                (if length fact = 1 then "" else "(" ^ string_of_int (i + 1) ^ ")")) ^
+              Position.here pos ^ "\n" ^ msg);
+          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
+          ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes prop))
+            handle TYPE (msg, _, _) => err msg
+              | TERM (msg, _) => err msg
+              | ERROR msg => err msg
+        end);
+    val arg = (b, Lazy.map_finished (tap check) fact);
   in
     thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
   end;