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);