# HG changeset patch # User wenzelm # Date 1526979947 -7200 # Node ID 37974ddde92844c3389aab7e2977b350f737568a # Parent ddf1ead7b182b3ba88d5c25dc4af71baa277c8bb# Parent e0cd57aeb60cc94954a8c422688a0c216653add5 merged diff -r ddf1ead7b182 -r 37974ddde928 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Mon May 21 18:36:30 2018 +0200 +++ b/src/Pure/global_theory.ML Tue May 22 11:05:47 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