# HG changeset patch
# User wenzelm
# Date 1526848620 -7200
# Node ID e0cd57aeb60cc94954a8c422688a0c216653add5
# Parent  eb57621568bb001175ffaa5e160e92fd89e3e6ac
more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);

diff -r eb57621568bb -r e0cd57aeb60c src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sun May 20 22:04:46 2018 +0200
+++ b/src/Pure/global_theory.ML	Sun May 20 22:37:00 2018 +0200
@@ -128,8 +128,19 @@
 
 fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
 
-fun add_facts arg thy =
-  thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2);
+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);
+  in
+    thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
+  end;
 
 fun add_thms_lazy kind (b, thms) thy =
   if Binding.is_empty b then Thm.register_proofs thms thy