src/Provers/quantifier1.ML

 sig
   val prove_one_point_all_tac: tactic
   val prove_one_point_ex_tac: tactic
   val rearrange_all: Proof.context -> cterm -> thm option
   val rearrange_ex: Proof.context -> cterm -> thm option
-  val rearrange_ball: tactic -> Proof.context -> cterm -> thm option
-  val rearrange_bex: tactic -> Proof.context -> cterm -> thm option
-  val rearrange_Collect: tactic -> Proof.context -> cterm -> thm option
+  val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+  val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+  val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
 end;
 
 functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
 struct
 

     fun exqu xs ((qC as Const (qa, _)) $ Abs (x, T, Q)) =
           if qa = q then exqu ((qC, x, T) :: xs) Q else NONE
       | exqu xs P = extract (null xs) xs P
   in exqu [] end;
 
-fun prove_conv tac ctxt tu =
+fun prove_conv ctxt tu tac =
   let
     val (goal, ctxt') =
       yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
     val thm =
-      Goal.prove ctxt' [] [] goal (K (rtac Data.iff_reflection 1 THEN tac));
+      Goal.prove ctxt' [] [] goal
+        (fn {context = ctxt'', ...} => rtac Data.iff_reflection 1 THEN tac ctxt'');
   in singleton (Variable.export ctxt' ctxt) thm end;
 
 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
 
 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)

     F as (all as Const (q, _)) $ Abs (x, T, P) =>
       (case extract_quant extract_imp q P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
           let val R = quantify all x T xs (Data.imp $ eq $ Q)
-          in SOME (prove_conv prove_one_point_all_tac ctxt (F, R)) end)
+          in SOME (prove_conv ctxt (F, R) (K prove_one_point_all_tac)) end)
   | _ => NONE);
 
 fun rearrange_ball tac ctxt ct =
   (case term_of ct of
     F as Ball $ A $ Abs (x, T, P) =>

         NONE => NONE
       | SOME (xs, eq, Q) =>
           if not (null xs) then NONE
           else
             let val R = Data.imp $ eq $ Q
-            in SOME (prove_conv tac ctxt (F, Ball $ A $ Abs (x, T, R))) end)
+            in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end)
   | _ => NONE);
 
 fun rearrange_ex ctxt ct =
   (case term_of ct of
     F as (ex as Const (q, _)) $ Abs (x, T, P) =>
       (case extract_quant extract_conj q P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
           let val R = quantify ex x T xs (Data.conj $ eq $ Q)
-          in SOME (prove_conv prove_one_point_ex_tac ctxt (F, R)) end)
+          in SOME (prove_conv ctxt (F, R) (K prove_one_point_ex_tac)) end)
   | _ => NONE);
 
 fun rearrange_bex tac ctxt ct =
   (case term_of ct of
     F as Bex $ A $ Abs (x, T, P) =>
       (case extract_conj true [] P of
         NONE => NONE
       | SOME (xs, eq, Q) =>
           if not (null xs) then NONE
-          else SOME (prove_conv tac ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))))
+          else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac))
   | _ => NONE);
 
 fun rearrange_Collect tac ctxt ct =
   (case term_of ct of
     F as Collect $ Abs (x, T, P) =>
       (case extract_conj true [] P of
         NONE => NONE
       | SOME (_, eq, Q) =>
           let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
-          in SOME (prove_conv tac ctxt (F, R)) end)
-  | _ => NONE);
-
-end;
-
+          in SOME (prove_conv ctxt (F, R) tac) end)
+  | _ => NONE);
+
+end;
+