1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 15 20:50:21 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 15 20:50:22 2006 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4        val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
     1.5  
     1.6        fun add_for_f fname psimps =
     1.7 -          LocalTheory.note ((NameSpace.append fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd
     1.8 +          LocalTheory.note ((NameSpace.qualified fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd
     1.9      in
    1.10        (saved_psimps,
    1.11         fold2 add_for_f fnames psimps_by_f lthy)
    1.12 @@ -68,7 +68,7 @@
    1.13        val Prep {f, R, ...} = data
    1.14        val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
    1.15        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    1.16 -      val qualify = NameSpace.append defname
    1.17 +      val qualify = NameSpace.qualified defname
    1.18            
    1.19        val (((psimps', pinducts'), (_, [termination'])), lthy) = 
    1.20            lthy
    1.21 @@ -141,7 +141,7 @@
    1.22          val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
    1.23          val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
    1.24          *)
    1.25 -        val qualify = NameSpace.append defname;
    1.26 +        val qualify = NameSpace.qualified defname;
    1.27      in
    1.28          lthy
    1.29            |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd