# HG changeset patch # User huffman # Date 1289360231 28800 # Node ID e380754e8a09d9dd639ccdeb19be20884e7a22c1 # Parent 6de5839e2fb3bfc9a50865db367b9faf0b047b37 adapt isodefl proof script to unpointed types diff -r 6de5839e2fb3 -r e380754e8a09 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Nov 09 16:37:13 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Nov 09 19:37:11 2010 -0800 @@ -645,8 +645,8 @@ @{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id}; val bottom_rules = @{thms fst_strict snd_strict isodefl_bottom simp_thms}; - val lthy = ProofContext.init_global thy; - val DEFL_simps = map (fn th => th RS sym) (RepData.get lthy); + val map_ID_thms = Domain_Take_Proofs.get_map_ID_thms thy; + val map_ID_simps = map (fn th => th RS sym) map_ID_thms; val isodefl_rules = @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL} @ isodefl_abs_rep_thms @@ -662,7 +662,7 @@ simp_tac (HOL_basic_ss addsimps bottom_rules) 1, simp_tac beta_ss 1, simp_tac (HOL_basic_ss addsimps @{thms fst_conv snd_conv}) 1, - simp_tac (HOL_basic_ss addsimps DEFL_simps) 1, + simp_tac (HOL_basic_ss addsimps map_ID_simps) 1, REPEAT (etac @{thm conjE} 1), REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)]) end;