fix proof script so qdomain_isomorphism foo = foo' works
authorhuffman
Fri, 05 Mar 2010 13:27:40 -0800
changeset 35589 a76cce4ad320
parent 35586 f57de4a9eb9c
child 35590 f638444c9667
fix proof script so qdomain_isomorphism foo = foo' works
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)