src/Pure/Thy/thm_database.ML
changeset 1308 396ef8aa37b7
parent 1272 dd877dc7c1f4
child 1512 ce37c64244c0
     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;