# HG changeset patch
# User huffman
# Date 1267824460 28800
# Node ID a76cce4ad3206c45d2f6e416cc306cbc07b2104b
# Parent  f57de4a9eb9c43fdb18dd1f97f44e24066483947
fix proof script so qdomain_isomorphism foo = foo' works

diff -r f57de4a9eb9c -r a76cce4ad320 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 05 09:27:47 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 05 13:27:40 2010 -0800
@@ -350,7 +350,7 @@
         val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT);
         val REP_simps = RepData.get thy;
         val tac =
-          simp_tac (HOL_basic_ss addsimps REP_simps) 1
+          rewrite_goals_tac (map mk_meta_eq REP_simps)
           THEN resolve_tac defl_unfold_thms 1;
       in
         Goal.prove_global thy [] [] goal (K tac)