--- a/src/HOL/Tools/Function/function_core.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Wed Oct 28 16:25:27 2009 +0100
@@ -488,7 +488,9 @@
|> Syntax.check_term lthy
val ((f, (_, f_defthm)), lthy) =
- LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy
+ LocalTheory.define Thm.internalK
+ ((Binding.name (function_name fname), mixfix),
+ ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
in
((f, f_defthm), lthy)
end