# HG changeset patch
# User huffman
# Date 1268535978 28800
# Node ID 98fd7910f70aa5a21624293fcf04963692907956
# Parent  7de1e14d9277017b0654091a9dfc594c22d2c5e2
use Simplifier.context to avoid 'no proof context in simpset' errors from fixrec_simp after theory merge

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);