# HG changeset patch
# User wenzelm
# Date 1030459261 -7200
# Node ID 7d62554fa0e0f7d3fa27650b8d8c1bb68c6dba95
# Parent  359c085c4def9a3b51a30ba25f4dadb34c77a053
disallow duplicate fact bindings for drafts (i.e. within new-style theory files);

diff -r 359c085c4def -r 7d62554fa0e0 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Aug 27 15:40:58 2002 +0200
+++ b/src/Pure/pure_thy.ML	Tue Aug 27 16:41:01 2002 +0200
@@ -234,6 +234,8 @@
         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));