# HG changeset patch
# User wenzelm
# Date 1258924231 -3600
# Node ID 1436dd2bd565764d60862d6f2df76116159913ea
# Parent  cf8365a709119b317891bc75830ac8f743dc9f11# Parent  91f3fc0364cf0dceb1124c354d4978fa8f1c69b1
merged

diff -r cf8365a70911 -r 1436dd2bd565 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 22 17:02:46 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 22 22:10:31 2009 +0100
@@ -519,7 +519,9 @@
           @{thms conjI isodefl_ID_REP}
           @ isodefl_abs_rep_thms
           @ IsodeflData.get thy;
-        fun tacf {prems, ...} = EVERY
+      in
+        Goal.prove_global thy [] assms goal (fn {prems, ...} =>
+         EVERY
           [simp_tac (HOL_basic_ss addsimps start_thms) 1,
            (* FIXME: how reliable is unification here? *)
            (* Maybe I should instantiate the rule. *)
@@ -529,9 +531,7 @@
            simp_tac beta_ss 1,
            simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
            REPEAT (etac @{thm conjE} 1),
-           REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)];
-      in
-        Goal.prove_global thy [] assms goal tacf
+           REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
       end;
     val isodefl_binds = map (Binding.prefix_name "isodefl_") dom_binds;
     fun conjuncts [] thm = []