src/HOL/Tools/Function/partial_function.ML

 
     val ((f_binding, fT), mixfix) = the_single fixes;
     val f_bname = Binding.name_of f_binding;
 
     fun note_qualified (name, thms) =
-      Local_Theory.note ((Binding.qualified true name (Binding.reset_pos f_binding), []), thms)
+      Local_Theory.note ((Binding.qualify_name true (Binding.reset_pos f_binding) name, []), thms)
         #> snd
 
     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn);
     val (head, args) = strip_comb lhs;
     val argnames = map (fst o dest_Free) args;