Slight simplification of code for pat/constr.

1 files changed, 3 insertions, 13 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d4480ec922..3e6cea5ddd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2216,19 +2216,9 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
           Proofview.tclUNIT () (* apply_in_once do a replacement *)
         else
           Proofview.V82.tactic (clear [id]) in
-      Proofview.Goal.enter begin fun gl ->
-        let sigma = Proofview.Goal.sigma gl in
-        let env = Proofview.Goal.env gl in
-        let sigma,c = f env sigma in
-        Tacticals.New.tclWITHHOLES false
-          (Tacticals.New.tclTHENFIRST
-             (* Skip the side conditions of the apply *)
-             (apply_in_once false true true true naming id
-                (None,(sigma,(c,NoBindings)))
-                (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id)))
-             (tac thin None []))
-          sigma
-      end
+      let f env sigma = let (sigma,c) = f env sigma in (sigma,(c,NoBindings)) in
+      apply_in_delayed_once false true true true naming id (None,(loc,f))
+        (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
 
 and prepare_intros_loc loc dft destopt = function
   | IntroNaming ipat ->