| changeset 40326 | 73d45866dbda |
| parent 40218 | f7d4d023a899 |
| child 40327 | 1dfdbd66093a |
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 29 16:24:07 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Oct 29 16:51:40 2010 -0700 @@ -38,7 +38,7 @@ struct val beta_rules = - @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @ + @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @ @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'}; val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);