merged
authorwenzelm
Tue May 22 11:05:47 2018 +0200 (21 months ago ago)
changeset 6824637974ddde928
parent 68243 ddf1ead7b182
parent 68245 e0cd57aeb60c
child 68247 b48bab511939
child 68248 7344affc0bd4
merged
     1.1 --- a/src/Pure/global_theory.ML	Mon May 21 18:36:30 2018 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Tue May 22 11:05:47 2018 +0200
     1.3 @@ -128,8 +128,19 @@
     1.4  
     1.5  fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
     1.6  
     1.7 -fun add_facts arg thy =
     1.8 -  thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2);
     1.9 +fun add_facts (b, fact) thy =
    1.10 +  let
    1.11 +    val full_name = Sign.full_name thy b;
    1.12 +    val pos = Binding.pos_of b;
    1.13 +    fun err msg =
    1.14 +      error ("Malformed global fact " ^ quote full_name ^ Position.here pos ^ "\n" ^ msg);
    1.15 +    fun check thm =
    1.16 +      ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes (Thm.full_prop_of thm)))
    1.17 +        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
    1.18 +    val arg = (b, Lazy.map_finished (tap (List.app check)) fact);
    1.19 +  in
    1.20 +    thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
    1.21 +  end;
    1.22  
    1.23  fun add_thms_lazy kind (b, thms) thy =
    1.24    if Binding.is_empty b then Thm.register_proofs thms thy