--- a/src/HOL/Tools/Function/function.ML Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML Wed Oct 29 19:01:49 2014 +0100
@@ -32,7 +32,6 @@
val termination : term option -> local_theory -> Proof.state
val termination_cmd : string option -> local_theory -> Proof.state
- val setup : theory -> theory
val get_congs : Proof.context -> thm list
val get_info : Proof.context -> term -> info
@@ -264,7 +263,6 @@
(* Datatype hook to declare datatype congs as "function_congs" *)
-
fun add_case_cong n thy =
let
val cong = #case_cong (Old_Datatype_Data.the_info thy n)
@@ -274,12 +272,10 @@
(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))
+val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_case_cong)))
-(* setup *)
-
-val setup = setup_case_cong
+(* get info *)
val get_congs = Function_Context_Tree.get_function_congs