sko/abs: Name.internal prevents choking of print_theory;
authorwenzelm
Tue Sep 19 23:15:32 2006 +0200 (2006-09-19)
changeset 20624ba081ac0ed7e
parent 20623 6ae83d153dd4
child 20625 1bb9a04f8c22
sko/abs: Name.internal prevents choking of print_theory;
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Sep 19 23:15:30 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Sep 19 23:15:32 2006 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4  fun declare_skofuns s th thy =
     1.5    let 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 = gensym ("sko_" ^ s ^ "_")
     1.8 +            let val cname = Name.internal (gensym ("sko_" ^ s ^ "_"))
     1.9                  val args = term_frees xtp  (*get the formal parameter list*)
    1.10                  val Ts = map type_of args
    1.11                  val cT = Ts ---> T
    1.12 @@ -276,7 +276,7 @@
    1.13          else
    1.14          case term_of ct of
    1.15            Abs (_,T,u) =>
    1.16 -            let val cname = gensym "abs_"
    1.17 +            let val cname = Name.internal (gensym "abs_");
    1.18                  val _ = assert_eta_free ct;
    1.19                  val (cv,cta) = Thm.dest_abs NONE ct
    1.20                  val v = (#1 o dest_Free o term_of) cv