tuned;
authorwenzelm
Sat Jul 27 21:47:43 2019 +0200 (3 weeks ago ago)
changeset 7061078514368ec63
parent 70609 4ed859e23025
child 70611 198be2de1efa
tuned;
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/global_theory.ML	Sat Jul 27 20:40:00 2019 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Sat Jul 27 21:47:43 2019 +0200
     1.3 @@ -181,23 +181,20 @@
     1.4        val thy'' = thy' |> add_facts (b, Lazy.value thms');
     1.5      in (map (Thm.transfer thy'') thms', thy'') end;
     1.6  
     1.7 -fun apply_fact pre_name post_name (b, fact) =
     1.8 -  apply_facts pre_name post_name (b, [fact]);
     1.9 -
    1.10  
    1.11  (* store_thm *)
    1.12  
    1.13  fun store_thm (b, th) =
    1.14 -  apply_fact (name_thms true true) (name_thms false true) (b, ([th], [])) #>> the_single;
    1.15 +  apply_facts (name_thms true true) (name_thms false true) (b, [([th], [])]) #>> the_single;
    1.16  
    1.17  fun store_thm_open (b, th) =
    1.18 -  apply_fact (name_thms true false) (name_thms false false) (b, ([th], [])) #>> the_single;
    1.19 +  apply_facts (name_thms true false) (name_thms false false) (b, [([th], [])]) #>> the_single;
    1.20  
    1.21  
    1.22  (* add_thms(s) *)
    1.23  
    1.24  fun add_thms_atts pre_name ((b, thms), atts) =
    1.25 -  apply_fact pre_name (name_thms false true) (b, (thms, atts));
    1.26 +  apply_facts pre_name (name_thms false true) (b, [(thms, atts)]);
    1.27  
    1.28  fun gen_add_thmss pre_name =
    1.29    fold_map (add_thms_atts pre_name);