src/HOL/Tools/specification_package.ML
changeset 14117 d3512dedbaea
parent 14116 63337d8e6e0f
child 14118 05416ba8eef2
--- 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