--- a/src/HOL/HOLCF/Domain_Aux.thy Thu Apr 10 12:22:29 2014 +0200
+++ b/src/HOL/HOLCF/Domain_Aux.thy Thu Apr 10 12:30:02 2014 +0200
@@ -350,6 +350,4 @@
ML_file "Tools/Domain/domain_constructors.ML"
ML_file "Tools/Domain/domain_induction.ML"
-setup Domain_Take_Proofs.setup
-
end
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Thu Apr 10 12:22:29 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Thu Apr 10 12:30:02 2014 +0200
@@ -61,7 +61,6 @@
val get_deflation_thms : theory -> thm list
val map_ID_add : attribute
val get_map_ID_thms : theory -> thm list
- val setup : theory -> theory
end
structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
@@ -148,7 +147,7 @@
val map_ID_add = Map_Id_Data.add
val get_map_ID_thms = Map_Id_Data.get o Proof_Context.init_global
-val setup = DeflMapData.setup #> Map_Id_Data.setup
+val _ = Theory.setup (DeflMapData.setup #> Map_Id_Data.setup)
(******************************************************************************)
(************************** building types and terms **************************)