# HG changeset patch
# User wenzelm
# Date 1397125802 -7200
# Node ID 265816f873868bc6748b298ea7d45738a38b83b8
# Parent  aec722524c3322b798cd5697f0df5fc452f99228
modernized theory setup;

diff -r aec722524c33 -r 265816f87386 src/HOL/HOLCF/Domain_Aux.thy
--- 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
diff -r aec722524c33 -r 265816f87386 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- 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 **************************)