use Named_Thms instead of Theory_Data for some domain package theorems

--- a/src/HOLCF/Domain_Aux.thy	Tue Oct 26 09:00:07 2010 -0700
+++ b/src/HOLCF/Domain_Aux.thy	Tue Oct 26 14:19:59 2010 -0700
@@ -260,4 +260,6 @@
 
 use "Tools/Domain/domain_take_proofs.ML"
 
+setup Domain_Take_Proofs.setup
+
 end

--- a/src/HOLCF/Library/Strict_Fun.thy	Tue Oct 26 09:00:07 2010 -0700
+++ b/src/HOLCF/Library/Strict_Fun.thy	Tue Oct 26 14:19:59 2010 -0700
@@ -69,7 +69,7 @@
 where
   "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
 
-lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
+lemma sfun_map_ID [domain_map_ID]: "sfun_map\<cdot>ID\<cdot>ID = ID"
   unfolding sfun_map_def
   by (simp add: cfun_map_ID cfun_eq_iff)
 
@@ -103,7 +103,7 @@
     done
 qed
 
-lemma deflation_sfun_map:
+lemma deflation_sfun_map [domain_deflation]:
   assumes 1: "deflation d1"
   assumes 2: "deflation d2"
   shows "deflation (sfun_map\<cdot>d1\<cdot>d2)"
@@ -198,11 +198,11 @@
 
 end
 
-lemma DEFL_sfun:
+lemma DEFL_sfun [domain_defl_simps]:
   "DEFL('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 by (rule defl_sfun_def)
 
-lemma isodefl_sfun:
+lemma isodefl_sfun [domain_isodefl]:
   "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
     isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
 apply (rule isodeflI)
@@ -213,8 +213,7 @@
 
 setup {*
   Domain_Isomorphism.add_type_constructor
-    (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm DEFL_sfun},
-       @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map})
+    (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map})
 *}
 
 end

--- a/src/HOLCF/Powerdomains.thy	Tue Oct 26 09:00:07 2010 -0700
+++ b/src/HOLCF/Powerdomains.thy	Tue Oct 26 14:19:59 2010 -0700
@@ -34,19 +34,18 @@
 
 subsection {* Domain package setup for powerdomains *}
 
+lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex
+lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID
+lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex
+
+lemmas [domain_deflation] =
+  deflation_upper_map deflation_lower_map deflation_convex_map
+
 setup {*
   fold Domain_Isomorphism.add_type_constructor
-    [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
-        @{thm DEFL_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
-          @{thm deflation_upper_map}),
-
-     (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
-        @{thm DEFL_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
-          @{thm deflation_lower_map}),
-
-     (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
-        @{thm DEFL_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
-          @{thm deflation_convex_map})]
+    [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}),
+     (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}),
+     (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map})]
 *}
 
 end

--- a/src/HOLCF/Representable.thy	Tue Oct 26 09:00:07 2010 -0700
+++ b/src/HOLCF/Representable.thy	Tue Oct 26 14:19:59 2010 -0700
@@ -267,22 +267,28 @@
 
 use "Tools/Domain/domain_isomorphism.ML"
 
+setup Domain_Isomorphism.setup
+
+lemmas [domain_defl_simps] =
+  DEFL_cfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
+
+lemmas [domain_map_ID] =
+  cfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
+
+lemmas [domain_isodefl] =
+  isodefl_cfun isodefl_ssum isodefl_sprod isodefl_cprod isodefl_u
+
+lemmas [domain_deflation] =
+  deflation_cfun_map deflation_ssum_map deflation_sprod_map
+  deflation_cprod_map deflation_u_map
+
 setup {*
   fold Domain_Isomorphism.add_type_constructor
-    [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm DEFL_cfun},
-        @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
-
-     (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm DEFL_ssum},
-        @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
-
-     (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm DEFL_sprod},
-        @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
-
-     (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm DEFL_prod},
-        @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
-
-     (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm DEFL_u},
-        @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})]
+    [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}),
+     (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}),
+     (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}),
+     (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}),
+     (@{type_name "u"}, @{term u_defl}, @{const_name u_map})]
 *}
 
 end

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Oct 26 09:00:07 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Oct 26 14:19:59 2010 -0700
@@ -28,7 +28,9 @@
     (string list * binding * mixfix * string * (binding * binding) option) list
       -> theory -> theory
   val add_type_constructor :
-    (string * term * string * thm  * thm * thm * thm) -> theory -> theory
+    (string * term * string) -> theory -> theory
+
+  val setup : theory -> theory
 end;
 
 structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
@@ -55,44 +57,31 @@
   fun merge data = Symtab.merge (K true) data;
 );
 
-structure RepData = Theory_Data
+structure RepData = Named_Thms
 (
-  (* theorems like "DEFL('a foo) = foo_defl$DEFL('a)" *)
-  type T = thm list;
-  val empty = [];
-  val extend = I;
-  val merge = Thm.merge_thms;
+  val name = "domain_defl_simps"
+  val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
+)
+
+structure MapIdData = Named_Thms
+(
+  val name = "domain_map_ID"
+  val description = "theorems like foo_map$ID = ID"
 );
 
-structure MapIdData = Theory_Data
+structure IsodeflData = Named_Thms
 (
-  (* theorems like "foo_map$ID = ID" *)
-  type T = thm list;
-  val empty = [];
-  val extend = I;
-  val merge = Thm.merge_thms;
-);
-
-structure IsodeflData = Theory_Data
-(
-  (* theorems like "isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" *)
-  type T = thm list;
-  val empty = [];
-  val extend = I;
-  val merge = Thm.merge_thms;
+  val name = "domain_isodefl"
+  val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
 );
 
 fun add_type_constructor
-  (tname, defl_const, map_name, DEFL_thm,
-   isodefl_thm, map_ID_thm, defl_map_thm) =
+  (tname, defl_const, map_name) =
     DeflData.map (Symtab.insert (K true) (tname, defl_const))
-    #> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm)
-    #> RepData.map (Thm.add_thm DEFL_thm)
-    #> IsodeflData.map (Thm.add_thm isodefl_thm)
-    #> MapIdData.map (Thm.add_thm map_ID_thm);
+    #> Domain_Take_Proofs.add_map_function (tname, map_name)
 
-
-(* val get_map_tab = MapData.get; *)
+val setup =
+    RepData.setup #> MapIdData.setup #> IsodeflData.setup
 
 
 (******************************************************************************)
@@ -357,15 +346,16 @@
 
     (* register map functions in theory data *)
     local
-      fun register_map ((dname, map_name), defl_thm) =
-          Domain_Take_Proofs.add_map_function (dname, map_name, defl_thm);
       val dnames = map (fst o dest_Type o fst) dom_eqns;
       val map_names = map (fst o dest_Const) map_consts;
     in
       val thy =
-          fold register_map (dnames ~~ map_names ~~ deflation_map_thms) thy;
+          fold Domain_Take_Proofs.add_map_function (dnames ~~ map_names) thy;
     end;
 
+    (* register deflation theorems *)
+    val thy = fold Domain_Take_Proofs.add_deflation_thm deflation_map_thms thy;
+
     val result =
       {
         map_consts = map_consts,
@@ -481,13 +471,13 @@
         (DEFL, thy)
       end;
     val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
-    val thy = RepData.map (fold Thm.add_thm DEFL_thms) thy;
+    val thy = fold (Context.theory_map o RepData.add_thm) DEFL_thms thy;
 
     (* prove DEFL equations *)
     fun mk_DEFL_eq_thm (lhsT, rhsT) =
       let
         val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT);
-        val DEFL_simps = RepData.get thy;
+        val DEFL_simps = RepData.get (ProofContext.init_global thy);
         val tac =
           rewrite_goals_tac (map mk_meta_eq DEFL_simps)
           THEN resolve_tac defl_unfold_thms 1;
@@ -582,11 +572,12 @@
           @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
         val bottom_rules =
           @{thms fst_strict snd_strict isodefl_bottom simp_thms};
-        val DEFL_simps = map (fn th => th RS sym) (RepData.get thy);
+        val lthy = ProofContext.init_global thy;
+        val DEFL_simps = map (fn th => th RS sym) (RepData.get lthy);
         val isodefl_rules =
           @{thms conjI isodefl_ID_DEFL}
           @ isodefl_abs_rep_thms
-          @ IsodeflData.get thy;
+          @ IsodeflData.get (ProofContext.init_global thy);
       in
         Goal.prove_global thy [] assms goal (fn {prems, ...} =>
          EVERY
@@ -612,7 +603,7 @@
     val (isodefl_thms, thy) = thy |>
       (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
         (conjuncts isodefl_binds isodefl_thm);
-    val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
+    val thy = fold (Context.theory_map o IsodeflData.add_thm) isodefl_thms thy;
 
     (* prove map_ID theorems *)
     fun prove_map_ID_thm
@@ -636,7 +627,7 @@
     val (_, thy) = thy |>
       (Global_Theory.add_thms o map Thm.no_attributes)
         (map_ID_binds ~~ map_ID_thms);
-    val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy;
+    val thy = fold (Context.theory_map o MapIdData.add_thm) map_ID_thms thy;
 
     (* definitions and proofs related to take functions *)
     val (take_info, thy) =
@@ -653,10 +644,11 @@
           list_ccomb (map_const, map mk_ID (snd (dest_Type lhsT)));
         val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns));
         val goal = mk_trp (mk_eq (lhs, rhs));
+        val map_ID_thms = MapIdData.get (ProofContext.init_global thy);
         val start_rules =
             @{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
             @ @{thms pair_collapse split_def}
-            @ map_apply_thms @ MapIdData.get thy;
+            @ map_apply_thms @ map_ID_thms;
         val rules0 =
             @{thms iterate_0 Pair_strict} @ take_0_thms;
         val rules1 =

--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Oct 26 09:00:07 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Oct 26 14:19:59 2010 -0700
@@ -55,11 +55,11 @@
   val map_of_typ :
     theory -> (typ * term) list -> typ -> term
 
-  val add_map_function :
-    (string * string * thm) -> theory -> theory
-
+  val add_map_function : (string * string) -> theory -> theory
   val get_map_tab : theory -> string Symtab.table
+  val add_deflation_thm : thm -> theory -> theory
   val get_deflation_thms : theory -> thm list
+  val setup : theory -> theory
 end;
 
 structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
@@ -126,21 +126,22 @@
   fun merge data = Symtab.merge (K true) data;
 );
 
-structure DeflMapData = Theory_Data
+structure DeflMapData = Named_Thms
 (
-  (* theorems like "deflation a ==> deflation (foo_map$a)" *)
-  type T = thm list;
-  val empty = [];
-  val extend = I;
-  val merge = Thm.merge_thms;
+  val name = "domain_deflation"
+  val description = "theorems like deflation a ==> deflation (foo_map$a)"
 );
 
-fun add_map_function (tname, map_name, deflation_map_thm) =
-    MapData.map (Symtab.insert (K true) (tname, map_name))
-    #> DeflMapData.map (Thm.add_thm deflation_map_thm);
+fun add_map_function (tname, map_name) =
+    MapData.map (Symtab.insert (K true) (tname, map_name));
+
+fun add_deflation_thm thm =
+    Context.theory_map (DeflMapData.add_thm thm);
 
 val get_map_tab = MapData.get;
-val get_deflation_thms = DeflMapData.get;
+fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy);
+
+val setup = DeflMapData.setup;
 
 (******************************************************************************)
 (************************** building types and terms **************************)
@@ -344,7 +345,7 @@
         val deflation_rules =
           @{thms conjI deflation_ID}
           @ deflation_abs_rep_thms
-          @ DeflMapData.get thy;
+          @ get_deflation_thms thy;
       in
         Goal.prove_global thy [] [] goal (fn _ =>
          EVERY