changeset 59498 | 50b60f501b05 |
parent 58977 | 9576b510f6a2 |
child 60555 | 51a6997b1384 |
--- a/src/CCL/Term.thy Tue Feb 10 14:29:36 2015 +0100 +++ b/src/CCL/Term.thy Tue Feb 10 14:48:26 2015 +0100 @@ -203,7 +203,7 @@ method_setup beta_rl = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED o - simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac @{thm letrecB})))) + simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB})))) *} lemma ifBtrue: "if true then t else u = t"