# HG changeset patch
# User wenzelm
# Date 1158700532 -7200
# Node ID ba081ac0ed7e50deeab9537361ce2d3ea44c6017
# Parent  6ae83d153dd43c4e67ca74a964486b9855e5320f
sko/abs: Name.internal prevents choking of print_theory;

diff -r 6ae83d153dd4 -r ba081ac0ed7e src/HOL/Tools/res_axioms.ML
--- 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