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