diff -r 677569668824 -r 5cb95b79a51f src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Wed Feb 12 08:35:56 2014 +0100 +++ b/src/HOL/Tools/Function/function.ML Wed Feb 12 08:35:56 2014 +0100 @@ -265,14 +265,14 @@ fun add_case_cong n thy = let - val cong = #case_cong (Datatype.the_info thy n) + val cong = #case_cong (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.interpretation (K (fold add_case_cong)) +val setup_case_cong = Datatype_Data.interpretation (K (fold add_case_cong)) (* setup *)