src/ZF/pair.thy

--- a/src/ZF/pair.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/ZF/pair.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -22,14 +22,14 @@
   fn _ => Quantifier1.rearrange_bex
     (fn ctxt =>
       unfold_tac ctxt @{thms Bex_def} THEN
-      Quantifier1.prove_one_point_ex_tac)
+      Quantifier1.prove_one_point_ex_tac ctxt)
 *}
 
 simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {*
   fn _ => Quantifier1.rearrange_ball
     (fn ctxt =>
       unfold_tac ctxt @{thms Ball_def} THEN
-      Quantifier1.prove_one_point_all_tac)
+      Quantifier1.prove_one_point_all_tac ctxt)
 *}