added check for duplicate theorems in theorem database;
changed warnings and error messages in thy_read to distinguish between
theorems in theor_y_ database and in theor_em_ database
--- a/src/Pure/Thy/thm_database.ML Mon Aug 21 18:03:12 1995 +0200
+++ b/src/Pure/Thy/thm_database.ML Wed Aug 30 14:04:39 1995 +0200
@@ -48,8 +48,8 @@
in distinct (consts t) end;
(*store a theorem in database*)
-fun store_thm_db (named_thm as (name, t)) =
- let val {prop, hyps, ...} = rep_thm t;
+fun store_thm_db (named_thm as (name, thm)) =
+ let val {prop, hyps, ...} = rep_thm thm;
val consts = distinct (flat (map list_consts (prop :: hyps)));
@@ -57,18 +57,33 @@
val tagged_thm = (num + 1, named_thm);
- fun update_db [] result = result
- | update_db (c :: cs) result =
- let val old_thms = Symtab.lookup_multi (result, c);
- in update_db cs (Symtab.update ((c, tagged_thm :: old_thms),
- result))
+ fun update_db _ [] result = result
+ | update_db warned (c :: cs) result =
+ let
+ val old_thms = Symtab.lookup_multi (result, c);
+
+ val warned' =
+ case find_first (fn (_, (n, _)) => n = name) old_thms of
+ Some (_, (_, t)) =>
+ if eq_thm (t, thm) then
+ (if not warned then
+ writeln ("Warning: Theorem database already \
+ \contains copy of theorem " ^ quote name)
+ else ();
+ true)
+ else error ("Duplicate theorem name " ^ quote name
+ ^ " used in theorem database")
+ | None => warned;
+ in update_db warned' cs
+ (if warned' then result
+ else (Symtab.update ((c, tagged_thm :: old_thms), result)))
end;
in if consts = [] then writeln ("Warning: Theorem " ^ name ^
" cannot be stored in ThmDB\n\t because it \
\contains no or only ignored constants.")
else ();
- thm_db := (num+1, update_db consts db);
- t
+ thm_db := (num+1, update_db false consts db);
+ thm
end;
(*intersection of two descending theorem lists*)
--- a/src/Pure/Thy/thy_read.ML Mon Aug 21 18:03:12 1995 +0200
+++ b/src/Pure/Thy/thy_read.ML Wed Aug 30 14:04:39 1995 +0200
@@ -501,13 +501,15 @@
let
val (thy_name, ThyInfo {path, children, thy_time, ml_time, theory, thms}) =
thyinfo_of_sign (#sign (rep_thm thm));
+
val thms' = Symtab.update_new ((name, thm), thms)
handle Symtab.DUPLICATE s =>
(if eq_thm (the (Symtab.lookup (thms, name)), thm) then
- (writeln ("Warning: Theorem database already contains copy of\
+ (writeln ("Warning: Theory database already contains copy of\
\ theorem " ^ quote name);
thms)
- else error ("Duplicate theorem name " ^ quote s));
+ else error ("Duplicate theorem name " ^ quote s
+ ^ " used in theory database"));
in
loaded_thys := Symtab.update
((thy_name, ThyInfo {path = path, children = children,