diff --git a/src/builtin/tactic.lua b/src/builtin/tactic.lua
index 6b5d23f15..436157449 100644
--- a/src/builtin/tactic.lua
+++ b/src/builtin/tactic.lua
@@ -31,15 +31,15 @@ tactic_macro("simp", { macro_arg.Ids },
 -- This tactic is useful for momentarily ignoring/skipping a "hole" in a big proof.
 -- Remark: the kernel will not accept a proof built using this tactic.
 skip_tac = tactic(function (env, ios, s)
-                     local gs      = s:goals()
-                     local pb      = s:proof_builder()
-                     local trivial = mk_constant("trivial")
-                     local new_pb  =
+                     local gs       = s:goals()
+                     local pb       = s:proof_builder()
+                     local buggy_pr = mk_constant("invalid proof built using skip tactic")
+                     local new_pb   =
                         function(m, a)
                            -- We provide a "fake/incorrect" proof for all goals in gs
                            local new_m = proof_map(m) -- Copy proof map m
                            for n, g in gs:pairs() do
-                              new_m:insert(n, trivial)
+                              new_m:insert(n, buggy_pr)
                            end
                            return pb(new_m, a)
                         end
diff --git a/tests/lean/jbug1.lean b/tests/lean/jbug1.lean
new file mode 100644
index 000000000..a4a75d9e5
--- /dev/null
+++ b/tests/lean/jbug1.lean
@@ -0,0 +1,12 @@
+import macros
+import tactic
+
+theorem le_iff (a b : Nat) : a ≤ b ↔ a < b ∨ a = b
+:=
+  iff_intro (
+    assume H : a ≤ b,
+    show a < b ∨ a = b, by skip
+  )(
+    assume H : a < b ∨ a = b,
+    show a ≤ b, by skip
+  )
\ No newline at end of file
diff --git a/tests/lean/jbug1.lean.expected.out b/tests/lean/jbug1.lean.expected.out
new file mode 100644
index 000000000..a5a4dbca7
--- /dev/null
+++ b/tests/lean/jbug1.lean.expected.out
@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'macros'
+  Imported 'tactic'
+jbug1.lean:4:0: error: unknown object 'invalid proof built using skip tactic'