diff -r 56cf1249ee20 -r bf5fcc65586b src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Sun Apr 17 16:36:47 2016 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Sun Apr 17 20:11:02 2016 +0200
@@ -230,7 +230,7 @@
     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);