diff -r ce378dcfddab -r abe0f11cfa4e src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Dec 05 18:42:39 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Dec 05 18:43:42 2008 +0100
@@ -96,8 +96,8 @@
 fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
     let
       val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
-      val fixes = map (apfst (apfst Name.name_of)) fixes0;
-      val spec = map (apfst (apfst Name.name_of)) spec0;
+      val fixes = map (apfst (apfst Binding.base_name)) fixes0;
+      val spec = map (apfst (apfst Binding.base_name)) spec0;
       val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
 
       val defname = mk_defname fixes