changeset 45654 | cf10bde35973 |
parent 43324 | 2b47822868e4 |
child 46909 | 3c73a121a387 |
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Nov 27 23:06:59 2011 +0100 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Nov 27 23:10:19 2011 +0100 @@ -381,7 +381,7 @@ @{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); +val beta_ss = HOL_basic_ss addsimps (@{thms simp_thms} @ beta_rules); fun define_consts (specs : (binding * term * mixfix) list)