src/HOL/Tools/Function/function.ML

--- a/src/HOL/Tools/Function/function.ML	Fri Sep 04 11:38:35 2015 +0200
+++ b/src/HOL/Tools/Function/function.ML	Fri Sep 04 13:39:20 2015 +0200
@@ -273,8 +273,7 @@
     val cong = #case_cong (Old_Datatype_Data.the_info thy n)
       |> safe_mk_meta_eq
   in
-    Context.theory_map
-      (Function_Context_Tree.map_function_congs (Thm.add_thm cong)) thy
+    Context.theory_map (Function_Context_Tree.add_function_cong cong) thy
   end
 
 val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_case_cong)))