src/CCL/Term.thy
changeset 51717 9e7d1c139569
parent 51670 d721d21e6374
child 52037 837211662fb8
--- a/src/CCL/Term.thy	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/CCL/Term.thy	Thu Apr 18 17:07:01 2013 +0200
@@ -204,7 +204,7 @@
 method_setup beta_rl = {*
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (CHANGED o
-      simp_tac (simpset_of ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB}))))
+      simp_tac (ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB}))))
 *}
 
 lemma ifBtrue: "if true then t else u = t"