src/CCL/Term.thy
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"