src/HOL/Tools/res_axioms.ML
changeset 30364 577edc39b501
parent 30291 a1c3abf57068
child 30510 4120fc59dd85
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -328,7 +328,7 @@
     1.4     "cases","ext_cases"];  (*FIXME: put other record thms here, or use the "Internal" marker*)
     1.5  
     1.6  (*Keep the full complexity of the original name*)
     1.7 -fun flatten_name s = space_implode "_X" (NameSpace.explode s);
     1.8 +fun flatten_name s = space_implode "_X" (Long_Name.explode s);
     1.9  
    1.10  fun fake_name th =
    1.11    if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
    1.12 @@ -340,7 +340,7 @@
    1.13  
    1.14  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
    1.15  fun skolem_thm (s, th) =
    1.16 -  if member (op =) multi_base_blacklist (NameSpace.base_name s) orelse bad_for_atp th then []
    1.17 +  if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then []
    1.18    else
    1.19      let
    1.20        val ctxt0 = Variable.thm_context th
    1.21 @@ -428,7 +428,7 @@
    1.22      val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) =>
    1.23        if already_seen thy name then I else cons (name, ths));
    1.24      val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
    1.25 -      if member (op =) multi_base_blacklist (NameSpace.base_name name) then I
    1.26 +      if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
    1.27        else fold_index (fn (i, th) =>
    1.28          if bad_for_atp th orelse is_some (lookup_cache thy th) then I
    1.29          else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);