--- a/src/HOL/Tools/Function/function.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Function/function.ML Mon Sep 01 16:17:46 2014 +0200
@@ -267,14 +267,14 @@
fun add_case_cong n thy =
let
- val cong = #case_cong (Datatype_Data.the_info thy n)
+ val cong = #case_cong (Old_Datatype_Data.the_info thy n)
|> safe_mk_meta_eq
in
Context.theory_map
(Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
end
-val setup_case_cong = Datatype_Data.interpretation (K (fold add_case_cong))
+val setup_case_cong = Old_Datatype_Data.interpretation (K (fold add_case_cong))
(* setup *)