# HG changeset patch
# User huffman
# Date 1267997693 28800
# Node ID 9617aeca7147d4b4dd5dfd1284a266611323a4a3
# Parent  e0b2a6e773db7d45fd842b76c9c779b942477a1d
fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'

diff -r e0b2a6e773db -r 9617aeca7147 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- 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;