diff -r 102e0e732495 -r 197e4df96fd4 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sun Sep 30 21:55:18 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Sun Sep 30 21:55:19 2007 +0200
@@ -87,13 +87,13 @@
   let val nref = ref 0
       fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
             (*Existential: declare a Skolem function, then insert into body and continue*)
-            let val cname = Name.internal ("sko_" ^ s ^ "_" ^ Int.toString (inc nref))
+            let val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref)
                 val args0 = term_frees xtp  (*get the formal parameter list*)
                 val Ts = map type_of args0
                 val extraTs = rhs_extra_types (Ts ---> T) xtp
                 val _ = if null extraTs then () else
-                   warning ("Skolemization: extra type vars: " ^ 
-                            commas_quote (map (Sign.string_of_typ thy) extraTs)); 
+                   warning ("Skolemization: extra type vars: " ^
+                            commas_quote (map (Sign.string_of_typ thy) extraTs));
                 val argsx = map (fn T => Free(gensym"vsk", T)) extraTs
                 val args = argsx @ args0
                 val cT = extraTs ---> Ts ---> T
@@ -246,7 +246,7 @@
         else
         case term_of ct of
           Abs _ =>
-            let val cname = Name.internal ("llabs_" ^ s ^ "_" ^ Int.toString (inc nref))
+            let val cname = "llabs_" ^ s ^ "_" ^ Int.toString (inc nref)
                 val _ = assert_eta_free ct;
                 val (cvs,cta) = dest_abs_list ct
                 val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
@@ -505,7 +505,7 @@
         (case skolem thy (Thm.transfer thy th) of
              NONE => ([th],thy)
            | SOME (cls,thy') =>
-                 (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ 
+                 (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^
                                          " clauses inserted into cache: " ^ name_or_string th);
                   (cls, ThmCache.put (Thmtab.update (th,cls) (ThmCache.get thy')) thy')))
     | SOME cls => (cls,thy);