replaced generic add by add_local/add_global;
authorwenzelm
Mon Mar 17 20:51:09 2008 +0100 (2008-03-17)
changeset 2630727d3de85c266
parent 26306 ed3375ac152d
child 26308 73d68876ba46
replaced generic add by add_local/add_global;
add_global: report/ignore duplicate bindings;
src/Pure/facts.ML
     1.1 --- a/src/Pure/facts.ML	Mon Mar 17 18:37:08 2008 +0100
     1.2 +++ b/src/Pure/facts.ML	Mon Mar 17 20:51:09 2008 +0100
     1.3 @@ -2,8 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Environment of named facts (admits overriding).  Optional indexing by
     1.8 -proposition.
     1.9 +Environment of named facts, optionally indexed by proposition.
    1.10  *)
    1.11  
    1.12  signature FACTS =
    1.13 @@ -17,7 +16,8 @@
    1.14    val could_unify: T -> term -> thm list
    1.15    val empty: T
    1.16    val merge: T * T -> T
    1.17 -  val add: bool -> NameSpace.naming -> string * thm list -> T -> T
    1.18 +  val add_global: NameSpace.naming -> string * thm list -> T -> T
    1.19 +  val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
    1.20    val del: string -> T -> T
    1.21  end;
    1.22  
    1.23 @@ -61,7 +61,7 @@
    1.24      val props' = Net.merge (is_equal o prop_ord) (props1, props2);
    1.25    in make_facts facts' props' end;
    1.26  
    1.27 -fun add do_props naming (name, ths) (Facts {facts, props}) =
    1.28 +fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
    1.29    let
    1.30      val facts' =
    1.31        if name = "" then facts
    1.32 @@ -69,13 +69,18 @@
    1.33          let
    1.34            val (space, tab) = facts;
    1.35            val space' = NameSpace.declare naming name space;
    1.36 -          val tab' = Symtab.update (name, ths) tab;
    1.37 +          val tab' = (if permissive then Symtab.update else Symtab.update_new) (name, ths) tab
    1.38 +            handle Symtab.DUP dup => (legacy_feature ("Duplicate fact " ^ quote dup ^
    1.39 +              Position.str_of (Position.thread_data ())); tab);
    1.40          in (space', tab') end;
    1.41      val props' =
    1.42        if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
    1.43        else props;
    1.44    in make_facts facts' props' end;
    1.45  
    1.46 +val add_global = add false false;
    1.47 +val add_local = add true;
    1.48 +
    1.49  fun del name (Facts {facts = (space, tab), props}) =
    1.50    let
    1.51      val space' = NameSpace.hide true name space handle ERROR _ => space;