diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean
index c18daf11d..76e542afb 100644
--- a/examples/lean/tactic_in_lua.lean
+++ b/examples/lean/tactic_in_lua.lean
@@ -65,7 +65,7 @@
 **)
 
 Theorem T (a b : Bool) : a => b => a /\ b := _.
-   apply (** REPEAT(ORELSE(imp_tac, conj_in_lua)) .. assumption_tac **)
+   apply (** THEN(REPEAT(ORELSE(imp_tac, conj_in_lua)), assumption_tac) **)
    done
 
 (* Show proof created using our script *)