# HG changeset patch
# User wenzelm
# Date 1117533196 -7200
# Node ID bd13a0017137756b52248ba9090fd4ee432240a4
# Parent  8340f7ca96d02bdd27808234642fa11b5cf700d9
proper use of Sign.full_name;

diff -r 8340f7ca96d0 -r bd13a0017137 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Tue May 31 11:53:15 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Tue May 31 11:53:16 2005 +0200
@@ -201,8 +201,7 @@
 		val args = term_frees xtp  (*get the formal parameter list*)
 		val Ts = map type_of args
 		val cT = Ts ---> T
-		val c = Const(NameSpace.append (PureThy.get_name thy) cname, cT)
-		        (*Generates a compound constant name in the given theory*)
+		val c = Const (Sign.full_name (Theory.sign_of thy) cname, cT)
 		val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
 		        (*Forms a lambda-abstraction over the formal parameters*)
 		val def = equals cT $ c $ rhs