# HG changeset patch
# User wenzelm
# Date 1208268731 -7200
# Node ID 1f711934f2217875eac371975cd2759e30bfb7b0
# Parent  60e0cf6bef896440826b01b71a927b3ea7156142
disallow duplicate entries (weak version for merge);
added hide;

diff -r 60e0cf6bef89 -r 1f711934f221 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Tue Apr 15 16:12:05 2008 +0200
+++ b/src/Pure/facts.ML	Tue Apr 15 16:12:11 2008 +0200
@@ -28,10 +28,11 @@
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
-  val del: string -> T -> T
   val add_global: NameSpace.naming -> string * thm list -> T -> T
   val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
   val add_dynamic: NameSpace.naming -> string * (Context.generic -> thm list) -> T -> T
+  val del: string -> T -> T
+  val hide: bool -> string -> T -> T
 end;
 
 structure Facts: FACTS =
@@ -159,23 +160,18 @@
 
 fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
 
+fun eq_entry ((Static ths1, _), (Static ths2, _)) = is_equal (list_ord Thm.thm_ord (ths1, ths2))
+  | eq_entry ((_, id1: serial), (_, id2)) = id1 = id2;
+
 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   let
-    (* FIXME authentic version
-    val facts' = NameSpace.merge_tables (eq_snd (op =)) (facts1, facts2)
-      handle Symtab.DUP dup => err_dup_fact dup; *)
-    val facts' = NameSpace.merge_tables (K true) (facts1, facts2)
+    val facts' = NameSpace.merge_tables eq_entry (facts1, facts2)
+      handle Symtab.DUP dup => err_dup_fact dup;
     val props' = Net.merge (is_equal o prop_ord) (props1, props2);
   in make_facts facts' props' end;
 
 
-(* static entries *)
-
-fun del name (Facts {facts = (space, tab), props}) =
-  let
-    val space' = NameSpace.hide true name space handle ERROR _ => space;
-    val tab' = Symtab.delete_safe name tab;
-  in make_facts (space', tab') props end;
+(* add static entries *)
 
 fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
   let
@@ -187,8 +183,7 @@
           val space' = NameSpace.declare naming name space;
           val entry = (name, (Static ths, serial ()));
           val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
-            handle Symtab.DUP dup => (legacy_feature ("Duplicate fact " ^ quote dup ^
-              Position.str_of (Position.thread_data ())); tab);
+            handle Symtab.DUP dup => err_dup_fact dup;
         in (space', tab') end;
     val props' =
       if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
@@ -199,7 +194,7 @@
 val add_local = add true;
 
 
-(* dynamic entries *)
+(* add dynamic entries *)
 
 fun add_dynamic naming (name, f) (Facts {facts = (space, tab), props}) =
   let
@@ -209,4 +204,16 @@
       handle Symtab.DUP dup => err_dup_fact dup;
   in make_facts (space', tab') props end;
 
+
+(* remove entries *)
+
+fun del name (Facts {facts = (space, tab), props}) =
+  let
+    val space' = NameSpace.hide true name space handle ERROR _ => space;
+    val tab' = Symtab.delete_safe name tab;
+  in make_facts (space', tab') props end;
+
+fun hide fully name (Facts {facts = (space, tab), props}) =
+  make_facts (NameSpace.hide fully name space, tab) props;
+
 end;