tuned Pure/General/name_space.ML
authorhaftmann
Thu May 24 08:37:37 2007 +0200 (2007-05-24)
changeset 2308612320f6e2523
parent 23085 fd30d75a6614
child 23087 ad7244663431
tuned Pure/General/name_space.ML
src/Pure/General/name_space.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/consts.ML
src/Pure/simplifier.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/General/name_space.ML	Thu May 24 07:27:44 2007 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Thu May 24 08:37:37 2007 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4      naming -> naming
     1.5    type 'a table (*= T * 'a Symtab.table*)
     1.6    val empty_table: 'a table
     1.7 -  val extend_table: naming -> 'a table * (bstring * 'a) list -> 'a table
     1.8 +  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
     1.9    val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    1.10    val dest_table: 'a table -> (string * 'a) list
    1.11    val extern_table: 'a table -> (xstring * 'a) list
    1.12 @@ -169,11 +169,8 @@
    1.13  (* basic operations *)
    1.14  
    1.15  fun map_space f xname (NameSpace tab) =
    1.16 -  let val entry' =
    1.17 -    (case Symtab.lookup tab xname of
    1.18 -      NONE => f ([], [])
    1.19 -    | SOME (entry, _) => f entry)
    1.20 -  in NameSpace (Symtab.update (xname, (entry', stamp ())) tab) end;
    1.21 +  NameSpace (Symtab.map_default (xname, (([], []), stamp ()))
    1.22 +    (fn (entry, _) => (f entry, stamp ())) tab);
    1.23  
    1.24  fun del (name: string) = remove (op =) name;
    1.25  fun add name names = name :: del name names;
    1.26 @@ -270,7 +267,7 @@
    1.27  
    1.28  val empty_table = (empty, Symtab.empty);
    1.29  
    1.30 -fun extend_table naming ((space, tab), bentries) =
    1.31 +fun extend_table naming bentries (space, tab) =
    1.32    let val entries = map (apfst (full naming)) bentries
    1.33    in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
    1.34  
     2.1 --- a/src/Pure/Isar/attrib.ML	Thu May 24 07:27:44 2007 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Thu May 24 08:37:37 2007 +0200
     2.3 @@ -127,7 +127,7 @@
     2.4    let
     2.5      val new_attrs =
     2.6        raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
     2.7 -    fun add attrs = NameSpace.extend_table (Sign.naming_of thy) (attrs, new_attrs)
     2.8 +    fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
     2.9        handle Symtab.DUPS dups =>
    2.10          error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
    2.11    in AttributesData.map add thy end;
     3.1 --- a/src/Pure/Isar/method.ML	Thu May 24 07:27:44 2007 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Thu May 24 08:37:37 2007 +0200
     3.3 @@ -423,7 +423,7 @@
     3.4      val new_meths = raw_meths |> map (fn (name, f, comment) =>
     3.5        (name, ((f, comment), stamp ())));
     3.6  
     3.7 -    fun add meths = NameSpace.extend_table (Sign.naming_of thy) (meths, new_meths)
     3.8 +    fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
     3.9        handle Symtab.DUPS dups =>
    3.10          error ("Duplicate declaration of method(s) " ^ commas_quote dups);
    3.11    in MethodsData.map add thy end;
     4.1 --- a/src/Pure/consts.ML	Thu May 24 07:27:44 2007 +0200
     4.2 +++ b/src/Pure/consts.ML	Thu May 24 08:37:37 2007 +0200
     4.3 @@ -202,7 +202,7 @@
     4.4  fun err_inconsistent_constraints cs =
     4.5    error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs);
     4.6  
     4.7 -fun extend_decls naming decl tab = NameSpace.extend_table naming (tab, [decl])
     4.8 +fun extend_decls naming decl tab = NameSpace.extend_table naming [decl] tab
     4.9    handle Symtab.DUPS cs => err_dup_consts cs;
    4.10  
    4.11  
     5.1 --- a/src/Pure/simplifier.ML	Thu May 24 07:27:44 2007 +0200
     5.2 +++ b/src/Pure/simplifier.ML	Thu May 24 08:37:37 2007 +0200
     5.3 @@ -228,7 +228,7 @@
     5.4        in
     5.5          context
     5.6          |> Simprocs.map (fn simprocs =>
     5.7 -            NameSpace.extend_table naming (simprocs, [(name', simproc')])
     5.8 +            NameSpace.extend_table naming [(name', simproc')] simprocs
     5.9                handle Symtab.DUPS ds => err_dup_simprocs ds)
    5.10          |> map_ss (fn ss => ss addsimprocs [simproc'])
    5.11        end)
     6.1 --- a/src/Pure/theory.ML	Thu May 24 07:27:44 2007 +0200
     6.2 +++ b/src/Pure/theory.ML	Thu May 24 08:37:37 2007 +0200
     6.3 @@ -181,7 +181,7 @@
     6.4  fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
     6.5    let
     6.6      val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms;
     6.7 -    val axioms' = NameSpace.extend_table (Sign.naming_of thy) (axioms, axms)
     6.8 +    val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
     6.9        handle Symtab.DUPS dups => err_dup_axms dups;
    6.10    in axioms' end);
    6.11  
    6.12 @@ -306,7 +306,7 @@
    6.13  (** add oracle **)
    6.14  
    6.15  fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles =>
    6.16 -  NameSpace.extend_table (Sign.naming_of thy) (oracles, [(bname, (oracle, stamp ()))])
    6.17 +  NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles
    6.18      handle Symtab.DUPS dups => err_dup_oras dups);
    6.19  
    6.20  end;