Removed "duplicate fact binding" error message.
--- a/src/Pure/pure_thy.ML Wed Feb 11 17:38:21 2004 +0100
+++ b/src/Pure/pure_thy.ML Wed Feb 11 17:39:00 2004 +0100
@@ -299,8 +299,6 @@
val named_thms = post_name name thms';
val r as ref {space, thms_tab, index} = get_theorems_sg sg;
- val _ = conditional (Sign.is_draft sg andalso is_some (Symtab.lookup (thms_tab, name)))
- (fn () => error ("Duplicate fact binding " ^ quote name));
val space' = NameSpace.extend (space, [name]);
val thms_tab' = Symtab.update ((name, named_thms), thms_tab);
val index' = FactIndex.add (K false) (index, (name, named_thms));