--- a/src/HOLCF/FOCUS/Buffer.thy Fri Mar 20 17:04:44 2009 +0100
+++ b/src/HOLCF/FOCUS/Buffer.thy Fri Mar 20 17:12:37 2009 +0100
@@ -98,8 +98,11 @@
by (erule subst, rule refl)
ML {*
-fun B_prover s tac eqs = prove_goal (the_context ()) s (fn prems => [cut_facts_tac prems 1,
- tac 1, auto_tac (claset(), simpset() addsimps eqs)]);
+fun B_prover s tac eqs =
+ let val thy = the_context () in
+ prove_goal thy s (fn prems => [cut_facts_tac prems 1,
+ tac 1, auto_tac (claset_of thy, simpset_of thy addsimps eqs)])
+ end;
fun prove_forw s thm = B_prover s (dtac (thm RS iffD1)) [];
fun prove_backw s thm eqs = B_prover s (rtac (thm RS iffD2)) eqs;