diff -r 49f602ae24e5 -r a5a91f387791 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/Pure/General/name_space.ML	Fri Dec 05 18:42:37 2008 +0100
@@ -48,7 +48,6 @@
     -> 'a table * 'a table -> 'a table
   val dest_table: 'a table -> (string * 'a) list
   val extern_table: 'a table -> (xstring * 'a) list
-  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
 end;
 
 structure NameSpace: NAME_SPACE =
@@ -303,10 +302,6 @@
     val (name, space') = declare naming b space;
   in (name, (space', Symtab.update_new (name, x) tab)) end;
 
-fun extend_table naming bentries (space, tab) =
-  let val entries = map (apfst (full_internal naming)) bentries
-  in (fold (declare_internal naming o #1) entries space, Symtab.extend (tab, entries)) end;
-
 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   (merge (space1, space2), Symtab.merge eq (tab1, tab2));