--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Fri Oct 29 16:51:40 2010 -0700
@@ -67,7 +67,7 @@
val simple_ss = HOL_basic_ss addsimps simp_thms;
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};
val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);