
diff -r 24971566ff4f -r 73d45866dbda src/HOLCF/ex/Pattern_Match.thy
--- a/src/HOLCF/ex/Pattern_Match.thy	Fri Oct 29 16:24:07 2010 -0700
+++ b/src/HOLCF/ex/Pattern_Match.thy	Fri Oct 29 16:51:40 2010 -0700
@@ -363,7 +363,7 @@
 infix 9 ` ;
 
 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);




