diff -r 7de1e14d9277 -r 98fd7910f70a src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Sat Mar 13 18:16:48 2010 -0800 +++ b/src/HOLCF/Tools/fixrec.ML Sat Mar 13 19:06:18 2010 -0800 @@ -305,7 +305,7 @@ fun fixrec_simp_tac ctxt = let val tab = FixrecUnfoldData.get (Context.Proof ctxt); - val ss = FixrecSimpData.get (Context.Proof ctxt); + val ss = Simplifier.context ctxt (FixrecSimpData.get (Context.Proof ctxt)); fun concl t = if Logic.is_all t then concl (snd (Logic.dest_all t)) else HOLogic.dest_Trueprop (Logic.strip_imp_concl t);