diff -r fd3f893a40ea -r aab139c0003f src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Wed Oct 29 11:41:54 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML	Wed Oct 29 13:42:38 2014 +0100
@@ -271,7 +271,7 @@
       |> safe_mk_meta_eq
   in
     Context.theory_map
-      (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
+      (Function_Context_Tree.map_function_congs (Thm.add_thm cong)) thy
   end
 
 val setup_case_cong = Old_Datatype_Data.interpretation (K (fold add_case_cong))
@@ -281,7 +281,7 @@
 
 val setup = setup_case_cong
 
-val get_congs = Function_Ctx_Tree.get_function_congs
+val get_congs = Function_Context_Tree.get_function_congs
 
 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
   |> the_single |> snd