Removed "duplicate fact binding" error message.
authorberghofe
Wed, 11 Feb 2004 17:39:00 +0100
changeset 14384 2128a8f0a676
parent 14383 09aab4710789
child 14385 6b15793a641a
Removed "duplicate fact binding" error message.
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));