src/Pure/General/name_space.ML
changeset 29004 a5a91f387791
parent 28991 694227dd3e8c
child 29338 52a384648d13
     1.1 --- a/src/Pure/General/name_space.ML	Fri Dec 05 11:42:27 2008 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Fri Dec 05 18:42:37 2008 +0100
     1.3 @@ -48,7 +48,6 @@
     1.4      -> 'a table * 'a table -> 'a table
     1.5    val dest_table: 'a table -> (string * 'a) list
     1.6    val extern_table: 'a table -> (xstring * 'a) list
     1.7 -  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
     1.8  end;
     1.9  
    1.10  structure NameSpace: NAME_SPACE =
    1.11 @@ -303,10 +302,6 @@
    1.12      val (name, space') = declare naming b space;
    1.13    in (name, (space', Symtab.update_new (name, x) tab)) end;
    1.14  
    1.15 -fun extend_table naming bentries (space, tab) =
    1.16 -  let val entries = map (apfst (full_internal naming)) bentries
    1.17 -  in (fold (declare_internal naming o #1) entries space, Symtab.extend (tab, entries)) end;
    1.18 -
    1.19  fun merge_tables eq ((space1, tab1), (space2, tab2)) =
    1.20    (merge (space1, space2), Symtab.merge eq (tab1, tab2));
    1.21