# HG changeset patch
# User skalberg
# Date 1058770326 -7200
# Node ID d3512dedbaea98aab2fe4a91c7d67fb8d9197c2e
# Parent  63337d8e6e0f82ae8632b87d89ed68c6bfc601dc
*** empty log message ***

diff -r 63337d8e6e0f -r d3512dedbaea src/HOL/Tools/specification_package.ML
--- 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