adapt isodefl proof script to unpointed types

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Nov 09 16:37:13 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Nov 09 19:37:11 2010 -0800
@@ -645,8 +645,8 @@
           @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
         val bottom_rules =
           @{thms fst_strict snd_strict isodefl_bottom simp_thms};
-        val lthy = ProofContext.init_global thy;
-        val DEFL_simps = map (fn th => th RS sym) (RepData.get lthy);
+        val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy;
+        val map_ID_simps = map (fn th => th RS sym) map_ID_thms;
         val isodefl_rules =
           @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL}
           @ isodefl_abs_rep_thms
@@ -662,7 +662,7 @@
            simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
            simp_tac beta_ss 1,
            simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
-           simp_tac (HOL_basic_ss addsimps DEFL_simps) 1,
+           simp_tac (HOL_basic_ss addsimps map_ID_simps) 1,
            REPEAT (etac @{thm conjE} 1),
            REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
       end;