diff --git a/src/defns.ml b/src/defns.ml
index 9a38bbf..b86e427 100644
--- a/src/defns.ml
+++ b/src/defns.ml
@@ -233,6 +233,11 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit =
             "\\text{"
             ^ String.concat "" (Grammar_pp.apply_hom_spec m xd hs [])
             ^ "}") in
+      Printf.fprintf fd "\\newcommand{\\%sRenameRule%s}[0]{%s{%s}}\n"
+        (Grammar_pp.pp_tex_NAME_PREFIX m)
+        (Grammar_pp.tex_command_escape dr.drule_name)
+        (Grammar_pp.pp_tex_DRULE_NAME_NAME m)
+        (Auxl.pp_tex_escape dr.drule_name);
       Printf.fprintf fd "\\newcommand{%s}[1]{%s[#1]{%%\n"
         (Grammar_pp.tex_drule_name m dr.drule_name)
         (Grammar_pp.pp_tex_DRULE_NAME m);
@@ -241,9 +246,9 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit =
         (snd ppd_premises);
       output_string fd "}{\n";
       output_string fd ppd_conclusion;
-      Printf.fprintf fd "}{%%\n{%s{%s}}{%s}%%\n}}\n"
-        (Grammar_pp.pp_tex_DRULE_NAME_NAME m)
-        (Auxl.pp_tex_escape dr.drule_name)
+      Printf.fprintf fd "}{%%\n{\\%sRenameRule%s}{%s}%%\n}}\n"
+        (Grammar_pp.pp_tex_NAME_PREFIX m)
+        (Grammar_pp.tex_command_escape dr.drule_name)   
         pp_com
   | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ ->
       let non_free_ntrs = Subrules_pp.non_free_ntrs m xd xd.xd_srs in