diff -r b3a9d8a83dea -r a8809f46bd7f src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 15 20:50:21 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 15 20:50:22 2006 +0100
@@ -55,7 +55,7 @@
       val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
 
       fun add_for_f fname psimps =
-          LocalTheory.note ((NameSpace.append fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd
+          LocalTheory.note ((NameSpace.qualified fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd
     in
       (saved_psimps,
        fold2 add_for_f fnames psimps_by_f lthy)
@@ -68,7 +68,7 @@
       val Prep {f, R, ...} = data
       val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
       val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
-      val qualify = NameSpace.append defname
+      val qualify = NameSpace.qualified defname
           
       val (((psimps', pinducts'), (_, [termination'])), lthy) = 
           lthy
@@ -141,7 +141,7 @@
         val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
         val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
         *)
-        val qualify = NameSpace.append defname;
+        val qualify = NameSpace.qualified defname;
     in
         lthy
           |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd