--- a/src/HOL/Tools/function_package/fundef_common.ML Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML Wed Mar 04 10:45:52 2009 +0100
@@ -82,7 +82,7 @@
psimps, pinducts, termination, defname}) phi =
let
val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
- val name = Binding.base_name o Morphism.binding phi o Binding.name
+ val name = Binding.name_of o Morphism.binding phi o Binding.name
in
FundefCtxData { add_simps = add_simps, case_names = case_names,
fs = map term fs, R = term R, psimps = fact psimps,