diff --git a/src/tac2compile.ml b/src/tac2compile.ml
index 3f4fff2..0d5cde2 100644
--- a/src/tac2compile.ml
+++ b/src/tac2compile.ml
@@ -898,7 +898,9 @@ let pp_one_constant (kn, knid, na, bnd, e) =
     | Fun (nas, e) ->
       hv 2
         (str "let " ++ h (str na ++ pp_binders nas) ++ str " =" ++ spc() ++
-         pp_expr e) ++ fnl() ++ fnl()
+         hov 2
+           (str "Tac2bt.with_frame (FrLtac " ++ SpilledKn.print knid ++ str ")"
+            ++ spc() ++ surround (pp_expr e))) ++ fnl() ++ fnl()
     | _ -> hv 2 (str "let " ++ str na ++ str " =" ++ spc() ++ pp_nontac_expr e) ++ fnl() ++ fnl()
   in
   let pp_set_compiled =