fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Mar 07 10:03:16 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Mar 07 13:34:53 2010 -0800
@@ -478,6 +478,7 @@
           @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
         val bottom_rules =
           @{thms fst_strict snd_strict isodefl_bottom simp_thms};
+        val REP_simps = map (fn th => th RS sym) (RepData.get thy);
         val isodefl_rules =
           @{thms conjI isodefl_ID_REP}
           @ isodefl_abs_rep_thms
@@ -493,6 +494,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 REP_simps) 1,
            REPEAT (etac @{thm conjE} 1),
            REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
       end;