changeset 52037 | 837211662fb8 |
parent 51717 | 9e7d1c139569 |
child 52143 | 36ffe23b25f8 |
--- 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"