--- 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;