tuned;
authorwenzelm
Sun Jul 28 12:35:59 2019 +0200 (3 weeks ago ago)
changeset 706134537e82019d3
parent 70612 973bf3e42e54
child 70614 7f7f149d6843
tuned;
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/global_theory.ML	Sun Jul 28 12:11:20 2019 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Sun Jul 28 12:35:59 2019 +0200
     1.3 @@ -206,17 +206,13 @@
     1.4  
     1.5  (* add_thms(s) *)
     1.6  
     1.7 -fun add_thms_atts pre_name ((b, thms), atts) =
     1.8 -  apply_facts pre_name (name_thms official2) (b, [(thms, atts)]);
     1.9 -
    1.10 -fun gen_add_thmss pre_name =
    1.11 -  fold_map (add_thms_atts pre_name);
    1.12 +val add_thmss =
    1.13 +  fold_map (fn ((b, thms), atts) =>
    1.14 +    apply_facts (name_thms official1) (name_thms official2) (b, [(thms, atts)]));
    1.15  
    1.16 -fun gen_add_thms pre_name args =
    1.17 -  apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
    1.18 +fun add_thms args =
    1.19 +  add_thmss (map (apfst (apsnd single)) args) #>> map the_single;
    1.20  
    1.21 -val add_thmss = gen_add_thmss (name_thms official1);
    1.22 -val add_thms = gen_add_thms (name_thms official1);
    1.23  val add_thm = yield_singleton add_thms;
    1.24  
    1.25  
    1.26 @@ -254,7 +250,11 @@
    1.27        |> Thm.forall_intr_frees
    1.28        |> Thm.forall_elim_vars 0
    1.29        |> Thm.varifyT_global;
    1.30 -  in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end);
    1.31 +  in
    1.32 +    thy'
    1.33 +    |> apply_facts (K I) (name_thms official2) (b, [([thm], atts)])
    1.34 +    |>> the_single
    1.35 +  end);
    1.36  
    1.37  in
    1.38