src/HOL/Tools/function_package/fundef_package.ML

 
       val saved_simps = flat (map snd saved_spec_simps)
       val simps_by_f = sort saved_simps
 
       fun add_for_f fname simps =
-        note_theorem ((NameSpace.qualified fname label, []), simps) #> snd
+        note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
     in
       (saved_simps,
        fold2 add_for_f fnames simps_by_f lthy)
     end
 

     let
       val FundefResult {fs, R, psimps, trsimps,  simple_pinducts, termination, domintros, cases, ...} = 
           cont (Thm.close_derivation proof)
 
       val fnames = map (fst o fst) fixes
-      val qualify = NameSpace.qualified defname
+      val qualify = Long_Name.qualify defname
       val addsmps = add_simps fnames post sort_cont
 
       val (((psimps', pinducts'), (_, [termination'])), lthy) =
           lthy
-            |> addsmps (NameSpace.qualified "partial") "psimps"
+            |> addsmps (Long_Name.qualify "partial") "psimps"
                        [Attrib.internal (K Nitpick_Const_Psimp_Thms.add)] psimps
             ||> fold_option (snd oo addsmps I "simps" [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]) trsimps
             ||>> note_theorem ((qualify "pinduct",
                    [Attrib.internal (K (RuleCases.case_names cnames)),
                     Attrib.internal (K (RuleCases.consumes 1)),

 
       val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
       val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
         [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
 
-      val qualify = NameSpace.qualified defname;
+      val qualify = Long_Name.qualify defname;
     in
       lthy
         |> add_simps I "simps" allatts tsimps |> snd
         |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd
     end