diff -r 25e9e7f527b4 -r f599ac41e7f5 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/HOL/Tools/Function/function.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -128,7 +128,7 @@
         val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
       in
         (info,
-         lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
+         lthy |> Local_Theory.declaration false (add_function_data o transform_function_data info))
       end
   in
     ((goal_state, afterqed), lthy')
@@ -203,7 +203,7 @@
             in
               (info',
                lthy 
-               |> Local_Theory.declaration false (add_function_data o morph_function_data info')
+               |> Local_Theory.declaration false (add_function_data o transform_function_data info')
                |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
             end)
         end