diff -r 890b68e1e8b6 -r f9d1442c70f3 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Mon Mar 30 22:34:59 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Mar 31 00:11:54 2015 +0200
@@ -262,7 +262,7 @@
     val inst_mono_thm = Thm.forall_elim (cert x_uc) mono_thm
 
     val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
-    val f_def_binding = Binding.conceal (Binding.name (Thm.def_name fname));
+    val f_def_binding = Binding.concealed (Binding.name (Thm.def_name fname));
     val ((f, (_, f_def)), lthy') = Local_Theory.define
       ((f_binding, mixfix), ((f_def_binding, []), f_def_rhs)) lthy;