--- 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 = []