diff -r 1aa2e40df9ff -r 837211662fb8 src/CCL/Term.thy --- a/src/CCL/Term.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/CCL/Term.thy Thu May 16 17:39:38 2013 +0200 @@ -204,7 +204,7 @@ method_setup beta_rl = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED o - simp_tac (ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB})))) + simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac @{thm letrecB})))) *} lemma ifBtrue: "if true then t else u = t"