# HG changeset patch
# User berghofe
# Date 1076517540 -3600
# Node ID 2128a8f0a676a9f1fcd603842ec229b50f872263
# Parent  09aab47107895b24ac314d52e14d5ad4161f2df0
Removed "duplicate fact binding" error message.

diff -r 09aab4710789 -r 2128a8f0a676 src/Pure/pure_thy.ML
--- 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));