diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sun Mar 08 17:19:15 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Sun Mar 08 17:26:14 2009 +0100
@@ -328,7 +328,7 @@
    "cases","ext_cases"];  (*FIXME: put other record thms here, or use the "Internal" marker*)
 
 (*Keep the full complexity of the original name*)
-fun flatten_name s = space_implode "_X" (NameSpace.explode s);
+fun flatten_name s = space_implode "_X" (Long_Name.explode s);
 
 fun fake_name th =
   if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
@@ -340,7 +340,7 @@
 
 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
 fun skolem_thm (s, th) =
-  if member (op =) multi_base_blacklist (NameSpace.base_name s) orelse bad_for_atp th then []
+  if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then []
   else
     let
       val ctxt0 = Variable.thm_context th
@@ -428,7 +428,7 @@
     val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) =>
       if already_seen thy name then I else cons (name, ths));
     val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
-      if member (op =) multi_base_blacklist (NameSpace.base_name name) then I
+      if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
       else fold_index (fn (i, th) =>
         if bad_for_atp th orelse is_some (lookup_cache thy th) then I
         else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);