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