src/Pure/facts.ML
changeset 33095 bbd52d2f8696
parent 33093 d010f61d3702
child 33096 db3c18fd9708
     1.1 --- a/src/Pure/facts.ML	Sat Oct 24 19:24:50 2009 +0200
     1.2 +++ b/src/Pure/facts.ML	Sat Oct 24 19:47:37 2009 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    val selections: string * thm list -> (ref * thm) list
     1.5    type T
     1.6    val empty: T
     1.7 -  val space_of: T -> NameSpace.T
     1.8 +  val space_of: T -> Name_Space.T
     1.9    val intern: T -> xstring -> string
    1.10    val extern: T -> string -> xstring
    1.11    val lookup: Context.generic -> T -> string -> (bool * thm list) option
    1.12 @@ -31,9 +31,9 @@
    1.13    val props: T -> thm list
    1.14    val could_unify: T -> term -> thm list
    1.15    val merge: T * T -> T
    1.16 -  val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
    1.17 -  val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
    1.18 -  val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
    1.19 +  val add_global: Name_Space.naming -> binding * thm list -> T -> string * T
    1.20 +  val add_local: bool -> Name_Space.naming -> binding * thm list -> T -> string * T
    1.21 +  val add_dynamic: Name_Space.naming -> binding * (Context.generic -> thm list) -> T -> string * T
    1.22    val del: string -> T -> T
    1.23    val hide: bool -> string -> T -> T
    1.24  end;
    1.25 @@ -122,11 +122,11 @@
    1.26  datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
    1.27  
    1.28  datatype T = Facts of
    1.29 - {facts: fact NameSpace.table,
    1.30 + {facts: fact Name_Space.table,
    1.31    props: thm Net.net};
    1.32  
    1.33  fun make_facts facts props = Facts {facts = facts, props = props};
    1.34 -val empty = make_facts NameSpace.empty_table Net.empty;
    1.35 +val empty = make_facts Name_Space.empty_table Net.empty;
    1.36  
    1.37  
    1.38  (* named facts *)
    1.39 @@ -136,8 +136,8 @@
    1.40  val space_of = #1 o facts_of;
    1.41  val table_of = #2 o facts_of;
    1.42  
    1.43 -val intern = NameSpace.intern o space_of;
    1.44 -val extern = NameSpace.extern o space_of;
    1.45 +val intern = Name_Space.intern o space_of;
    1.46 +val extern = Name_Space.extern o space_of;
    1.47  
    1.48  val defined = Symtab.defined o table_of;
    1.49  
    1.50 @@ -177,7 +177,7 @@
    1.51  
    1.52  fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
    1.53    let
    1.54 -    val facts' = NameSpace.merge_tables (facts1, facts2);
    1.55 +    val facts' = Name_Space.merge_tables (facts1, facts2);
    1.56      val props' = Net.merge (is_equal o prop_ord) (props1, props2);
    1.57    in make_facts facts' props' end;
    1.58  
    1.59 @@ -190,7 +190,7 @@
    1.60    let
    1.61      val (name, facts') =
    1.62        if Binding.is_empty b then ("", facts)
    1.63 -      else NameSpace.define strict naming (b, Static ths) facts;
    1.64 +      else Name_Space.define strict naming (b, Static ths) facts;
    1.65      val props' =
    1.66        if do_props
    1.67        then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
    1.68 @@ -208,7 +208,7 @@
    1.69  (* add dynamic entries *)
    1.70  
    1.71  fun add_dynamic naming (b, f) (Facts {facts, props}) =
    1.72 -  let val (name, facts') = NameSpace.define true naming (b, Dynamic f) facts;
    1.73 +  let val (name, facts') = Name_Space.define true naming (b, Dynamic f) facts;
    1.74    in (name, make_facts facts' props) end;
    1.75  
    1.76  
    1.77 @@ -216,11 +216,11 @@
    1.78  
    1.79  fun del name (Facts {facts = (space, tab), props}) =
    1.80    let
    1.81 -    val space' = NameSpace.hide true name space handle ERROR _ => space;  (* FIXME handle?? *)
    1.82 +    val space' = Name_Space.hide true name space handle ERROR _ => space;  (* FIXME handle?? *)
    1.83      val tab' = Symtab.delete_safe name tab;
    1.84    in make_facts (space', tab') props end;
    1.85  
    1.86  fun hide fully name (Facts {facts = (space, tab), props}) =
    1.87 -  make_facts (NameSpace.hide fully name space, tab) props;
    1.88 +  make_facts (Name_Space.hide fully name space, tab) props;
    1.89  
    1.90  end;