modernized theory setup;
authorwenzelm
Thu, 10 Apr 2014 12:30:02 +0200
changeset 56511 265816f87386
parent 56510 aec722524c33
child 56512 9276da80f7c3
modernized theory setup;
src/HOL/HOLCF/Domain_Aux.thy
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- 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 **************************)