1.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 22 17:02:46 2009 +0100
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 22 22:10:31 2009 +0100
     1.3 @@ -519,7 +519,9 @@
     1.4            @{thms conjI isodefl_ID_REP}
     1.5            @ isodefl_abs_rep_thms
     1.6            @ IsodeflData.get thy;
     1.7 -        fun tacf {prems, ...} = EVERY
     1.8 +      in
     1.9 +        Goal.prove_global thy [] assms goal (fn {prems, ...} =>
    1.10 +         EVERY
    1.11            [simp_tac (HOL_basic_ss addsimps start_thms) 1,
    1.12             (* FIXME: how reliable is unification here? *)
    1.13             (* Maybe I should instantiate the rule. *)
    1.14 @@ -529,9 +531,7 @@
    1.15             simp_tac beta_ss 1,
    1.16             simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1,
    1.17             REPEAT (etac @{thm conjE} 1),
    1.18 -           REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)];
    1.19 -      in
    1.20 -        Goal.prove_global thy [] assms goal tacf
    1.21 +           REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
    1.22        end;
    1.23      val isodefl_binds = map (Binding.prefix_name "isodefl_") dom_binds;
    1.24      fun conjuncts [] thm = []