diff -r 0c5cd369a643 -r 50b60f501b05 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/ZF/OrdQuant.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -370,14 +370,14 @@
   fn _ => Quantifier1.rearrange_bex
     (fn ctxt =>
       unfold_tac ctxt @{thms rex_def} THEN
-      Quantifier1.prove_one_point_ex_tac)
+      Quantifier1.prove_one_point_ex_tac ctxt)
 *}
 
 simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = {*
   fn _ => Quantifier1.rearrange_ball
     (fn ctxt =>
       unfold_tac ctxt @{thms rall_def} THEN
-      Quantifier1.prove_one_point_all_tac)
+      Quantifier1.prove_one_point_all_tac ctxt)
 *}
 
 end