1.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Sep 30 21:55:18 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Sep 30 21:55:19 2007 +0200
     1.3 @@ -87,13 +87,13 @@
     1.4    let val nref = ref 0
     1.5        fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
     1.6              (*Existential: declare a Skolem function, then insert into body and continue*)
     1.7 -            let val cname = Name.internal ("sko_" ^ s ^ "_" ^ Int.toString (inc nref))
     1.8 +            let val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref)
     1.9                  val args0 = term_frees xtp  (*get the formal parameter list*)
    1.10                  val Ts = map type_of args0
    1.11                  val extraTs = rhs_extra_types (Ts ---> T) xtp
    1.12                  val _ = if null extraTs then () else
    1.13 -                   warning ("Skolemization: extra type vars: " ^ 
    1.14 -                            commas_quote (map (Sign.string_of_typ thy) extraTs)); 
    1.15 +                   warning ("Skolemization: extra type vars: " ^
    1.16 +                            commas_quote (map (Sign.string_of_typ thy) extraTs));
    1.17                  val argsx = map (fn T => Free(gensym"vsk", T)) extraTs
    1.18                  val args = argsx @ args0
    1.19                  val cT = extraTs ---> Ts ---> T
    1.20 @@ -246,7 +246,7 @@
    1.21          else
    1.22          case term_of ct of
    1.23            Abs _ =>
    1.24 -            let val cname = Name.internal ("llabs_" ^ s ^ "_" ^ Int.toString (inc nref))
    1.25 +            let val cname = "llabs_" ^ s ^ "_" ^ Int.toString (inc nref)
    1.26                  val _ = assert_eta_free ct;
    1.27                  val (cvs,cta) = dest_abs_list ct
    1.28                  val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
    1.29 @@ -505,7 +505,7 @@
    1.30          (case skolem thy (Thm.transfer thy th) of
    1.31               NONE => ([th],thy)
    1.32             | SOME (cls,thy') =>
    1.33 -                 (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ 
    1.34 +                 (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^
    1.35                                           " clauses inserted into cache: " ^ name_or_string th);
    1.36                    (cls, ThmCache.put (Thmtab.update (th,cls) (ThmCache.get thy')) thy')))
    1.37      | SOME cls => (cls,thy);