src/Pure/pure_thy.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18614 3618d5ae0ac8
     1.1 --- a/src/Pure/pure_thy.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -308,8 +308,8 @@
     1.4  fun name_thmss name xs =
     1.5    (case filter_out (null o fst) xs of
     1.6      [([x], z)] => [([name_thm true (name, x)], z)]
     1.7 -  | _ => snd (foldl_map (fn (i, (ys, z)) =>
     1.8 -    (i + length ys, (map (name_thm true) (gen_names i (length ys) name ~~ ys), z))) (0, xs)));
     1.9 +  | _ => fst (fold_map (fn (ys, z) => fn i =>
    1.10 +    ((map (name_thm true) (gen_names i (length ys) name ~~ ys), z), i + length ys)) xs 0));
    1.11  
    1.12  
    1.13  (* enter_thms *)
    1.14 @@ -317,7 +317,7 @@
    1.15  fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
    1.16  fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
    1.17  
    1.18 -fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms)
    1.19 +fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) |> swap
    1.20    | enter_thms pre_name post_name app_att (bname, thms) thy =
    1.21        let
    1.22          val name = Sign.full_name thy bname;
    1.23 @@ -333,15 +333,15 @@
    1.24              if Thm.eq_thms (thms', thms'') then warn_same name
    1.25              else warn_overwrite name);
    1.26          r := {theorems = (space', theorems'), index = index'};
    1.27 -        (thy', thms')
    1.28 +        (thms', thy')
    1.29        end;
    1.30  
    1.31  
    1.32  (* add_thms(s) *)
    1.33  
    1.34  fun add_thms_atts pre_name ((bname, thms), atts) =
    1.35 -  swap o enter_thms pre_name (name_thms false)
    1.36 -    (Thm.applys_attributes o rpair atts) (bname, thms);
    1.37 +  enter_thms pre_name (name_thms false)
    1.38 +    (Thm.applys_attributes atts) (bname, thms);
    1.39  
    1.40  fun gen_add_thmss pre_name =
    1.41    fold_map (add_thms_atts pre_name);
    1.42 @@ -357,21 +357,21 @@
    1.43  
    1.44  local
    1.45  
    1.46 -fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
    1.47 +fun gen_note_thss get kind_att ((bname, more_atts), ths_atts) thy =
    1.48    let
    1.49 -    fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
    1.50 -    val (thy', thms) = thy |> enter_thms
    1.51 +    fun app (x, (ths, atts)) = Thm.applys_attributes atts (x, ths);
    1.52 +    val (thms, thy') = thy |> enter_thms
    1.53        name_thmss (name_thms false) (apsnd List.concat o foldl_map app)
    1.54        (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
    1.55 -  in (thy', (bname, thms)) end;
    1.56 +  in ((bname, thms), thy') end;
    1.57  
    1.58 -fun gen_note_thmss get kind_att args thy =
    1.59 -  foldl_map (gen_note_thss get kind_att) (thy, args);
    1.60 +fun gen_note_thmss get kind_att =
    1.61 +  fold_map (gen_note_thss get kind_att);
    1.62  
    1.63  in
    1.64  
    1.65 -val note_thmss = swap ooo gen_note_thmss get_thms;
    1.66 -val note_thmss_i = swap ooo gen_note_thmss (K I);
    1.67 +val note_thmss = gen_note_thmss get_thms;
    1.68 +val note_thmss_i = gen_note_thmss (K I);
    1.69  
    1.70  end;
    1.71  
    1.72 @@ -390,12 +390,12 @@
    1.73  fun smart_store _ (name, []) =
    1.74        error ("Cannot store empty list of theorems: " ^ quote name)
    1.75    | smart_store name_thm (name, [thm]) =
    1.76 -      #2 (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
    1.77 +      fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
    1.78    | smart_store name_thm (name, thms) =
    1.79        let
    1.80          fun merge (thy, th) = Theory.merge (thy, Thm.theory_of_thm th);
    1.81          val thy = Library.foldl merge (Thm.theory_of_thm (hd thms), tl thms);
    1.82 -      in #2 (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
    1.83 +      in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
    1.84  
    1.85  in
    1.86