removed "duplicate" warning from store_thm_db;
authorclasohm
Wed Oct 25 13:41:45 1995 +0100 (1995-10-25)
changeset 1308396ef8aa37b7
parent 1307 63a5788774f7
child 1309 890303a7bbc8
removed "duplicate" warning from store_thm_db;
changed place where store_thm_db is called for a theory's axioms
src/Pure/Thy/thm_database.ML
src/Pure/Thy/thy_read.ML
     1.1 --- a/src/Pure/Thy/thm_database.ML	Wed Oct 25 12:53:53 1995 +0100
     1.2 +++ b/src/Pure/Thy/thm_database.ML	Wed Oct 25 13:41:45 1995 +0100
     1.3 @@ -80,10 +80,7 @@
     1.4                  else case find_first (fn (_, (n, _)) => n = name) old_thms of
     1.5                         Some (_, (_, t)) => eq_thm (t, thm)
     1.6                       | None => false
     1.7 -            in if duplicate then
     1.8 -                 (writeln ("Warning: Theorem database already contains copy of\
     1.9 -                           \ theorem " ^ quote name);
    1.10 -                  None)
    1.11 +            in if duplicate then None
    1.12                 else update_db true
    1.13                        cs (Symtab.update ((c, tagged_thm :: old_thms), result))
    1.14              end;
     2.1 --- a/src/Pure/Thy/thy_read.ML	Wed Oct 25 12:53:53 1995 +0100
     2.2 +++ b/src/Pure/Thy/thy_read.ML	Wed Oct 25 13:41:45 1995 +0100
     2.3 @@ -627,6 +627,17 @@
     2.4            use (out_name tname);
     2.5            save_thy_ss ();
     2.6  
     2.7 +          (*Store axioms of theory
     2.8 +            (but only if it's not a copy of an older theory)*)
     2.9 +          let val parents = parents_of tname;
    2.10 +              val this_thy = theory_of tname;
    2.11 +              val axioms =
    2.12 +                if length parents = 1
    2.13 +                   andalso Sign.eq_sg (sign_of (theory_of (hd parents)),
    2.14 +                                       sign_of this_thy) then []
    2.15 +                else axioms_of this_thy;
    2.16 +          in map store_thm_db axioms end;
    2.17 +
    2.18            if not (!delete_tmpfiles) then ()
    2.19            else delete_file (out_name tname);
    2.20  
    2.21 @@ -646,17 +657,6 @@
    2.22         use_string
    2.23           ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
    2.24  
    2.25 -       (*Store axioms of theory
    2.26 -         (but only if it's not a copy of an older theory)*)
    2.27 -       let val parents = parents_of tname;
    2.28 -           val this_thy = theory_of tname;
    2.29 -           val axioms =
    2.30 -             if length parents = 1
    2.31 -                andalso Sign.eq_sg (sign_of (theory_of (hd parents)),
    2.32 -                                    sign_of this_thy) then []
    2.33 -             else axioms_of this_thy;
    2.34 -       in map store_thm_db axioms end;
    2.35 -
    2.36         (*Add theory to list of all loaded theories (for 00-chart.html)
    2.37           and add it to its parents' sub-charts*)
    2.38         if !make_html then