--- 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);