1.1 --- a/src/HOL/Tools/specification_package.ML	Sat Jul 19 17:35:15 2003 +0200
     1.2 +++ b/src/HOL/Tools/specification_package.ML	Mon Jul 21 08:52:06 2003 +0200
     1.3 @@ -43,10 +43,11 @@
     1.4  	Const("Trueprop",_) $ (Const("Ex",_) $ P) =>
     1.5  	let
     1.6  	    val ctype = domain_type (type_of P)
     1.7 +	    val cname_full = Sign.intern_const (sign_of thy) cname
     1.8  	    val cdefname = if thname = ""
     1.9  			   then Thm.def_name (Sign.base_name cname)
    1.10  			   else thname
    1.11 -	    val def_eq = Logic.mk_equals (Const(cname,ctype),choice_const ctype $  P)
    1.12 +	    val def_eq = Logic.mk_equals (Const(cname_full,ctype),choice_const ctype $  P)
    1.13  	    val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy
    1.14  	    val thm' = [thm,hd thms] MRS helper
    1.15  	in