sko/abs: Name.internal prevents choking of print_theory;

--- a/src/HOL/Tools/res_axioms.ML	Tue Sep 19 23:15:30 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Tue Sep 19 23:15:32 2006 +0200
@@ -139,7 +139,7 @@
 fun declare_skofuns s th thy =
   let 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 = gensym ("sko_" ^ s ^ "_")
+            let val cname = Name.internal (gensym ("sko_" ^ s ^ "_"))
                 val args = term_frees xtp  (*get the formal parameter list*)
                 val Ts = map type_of args
                 val cT = Ts ---> T
@@ -276,7 +276,7 @@
         else
         case term_of ct of
           Abs (_,T,u) =>
-            let val cname = gensym "abs_"
+            let val cname = Name.internal (gensym "abs_");
                 val _ = assert_eta_free ct;
                 val (cv,cta) = Thm.dest_abs NONE ct
                 val v = (#1 o dest_Free o term_of) cv