# HG changeset patch # User haftmann # Date 1179988657 -7200 # Node ID 12320f6e25234db2a3a681b1e3bdd12cbcc7a25b # Parent fd30d75a66142c8c80c060a2ec5dd1ca6c35d946 tuned Pure/General/name_space.ML diff -r fd30d75a6614 -r 12320f6e2523 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Thu May 24 07:27:44 2007 +0200 +++ b/src/Pure/General/name_space.ML Thu May 24 08:37:37 2007 +0200 @@ -53,7 +53,7 @@ naming -> naming type 'a table (*= T * 'a Symtab.table*) val empty_table: 'a table - val extend_table: naming -> 'a table * (bstring * 'a) list -> 'a table + val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table val dest_table: 'a table -> (string * 'a) list val extern_table: 'a table -> (xstring * 'a) list @@ -169,11 +169,8 @@ (* basic operations *) fun map_space f xname (NameSpace tab) = - let val entry' = - (case Symtab.lookup tab xname of - NONE => f ([], []) - | SOME (entry, _) => f entry) - in NameSpace (Symtab.update (xname, (entry', stamp ())) tab) end; + NameSpace (Symtab.map_default (xname, (([], []), stamp ())) + (fn (entry, _) => (f entry, stamp ())) tab); fun del (name: string) = remove (op =) name; fun add name names = name :: del name names; @@ -270,7 +267,7 @@ val empty_table = (empty, Symtab.empty); -fun extend_table naming ((space, tab), bentries) = +fun extend_table naming bentries (space, tab) = let val entries = map (apfst (full naming)) bentries in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end; diff -r fd30d75a6614 -r 12320f6e2523 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu May 24 07:27:44 2007 +0200 +++ b/src/Pure/Isar/attrib.ML Thu May 24 08:37:37 2007 +0200 @@ -127,7 +127,7 @@ let val new_attrs = raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ()))); - fun add attrs = NameSpace.extend_table (Sign.naming_of thy) (attrs, new_attrs) + fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs handle Symtab.DUPS dups => error ("Duplicate declaration of attributes(s) " ^ commas_quote dups); in AttributesData.map add thy end; diff -r fd30d75a6614 -r 12320f6e2523 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu May 24 07:27:44 2007 +0200 +++ b/src/Pure/Isar/method.ML Thu May 24 08:37:37 2007 +0200 @@ -423,7 +423,7 @@ val new_meths = raw_meths |> map (fn (name, f, comment) => (name, ((f, comment), stamp ()))); - fun add meths = NameSpace.extend_table (Sign.naming_of thy) (meths, new_meths) + fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths handle Symtab.DUPS dups => error ("Duplicate declaration of method(s) " ^ commas_quote dups); in MethodsData.map add thy end; diff -r fd30d75a6614 -r 12320f6e2523 src/Pure/consts.ML --- a/src/Pure/consts.ML Thu May 24 07:27:44 2007 +0200 +++ b/src/Pure/consts.ML Thu May 24 08:37:37 2007 +0200 @@ -202,7 +202,7 @@ fun err_inconsistent_constraints cs = error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs); -fun extend_decls naming decl tab = NameSpace.extend_table naming (tab, [decl]) +fun extend_decls naming decl tab = NameSpace.extend_table naming [decl] tab handle Symtab.DUPS cs => err_dup_consts cs; diff -r fd30d75a6614 -r 12320f6e2523 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Thu May 24 07:27:44 2007 +0200 +++ b/src/Pure/simplifier.ML Thu May 24 08:37:37 2007 +0200 @@ -228,7 +228,7 @@ in context |> Simprocs.map (fn simprocs => - NameSpace.extend_table naming (simprocs, [(name', simproc')]) + NameSpace.extend_table naming [(name', simproc')] simprocs handle Symtab.DUPS ds => err_dup_simprocs ds) |> map_ss (fn ss => ss addsimprocs [simproc']) end) diff -r fd30d75a6614 -r 12320f6e2523 src/Pure/theory.ML --- a/src/Pure/theory.ML Thu May 24 07:27:44 2007 +0200 +++ b/src/Pure/theory.ML Thu May 24 08:37:37 2007 +0200 @@ -181,7 +181,7 @@ fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms => let val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms; - val axioms' = NameSpace.extend_table (Sign.naming_of thy) (axioms, axms) + val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms handle Symtab.DUPS dups => err_dup_axms dups; in axioms' end); @@ -306,7 +306,7 @@ (** add oracle **) fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles => - NameSpace.extend_table (Sign.naming_of thy) (oracles, [(bname, (oracle, stamp ()))]) + NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles handle Symtab.DUPS dups => err_dup_oras dups); end;