diff --git a/src/mmhlpb.c b/src/mmhlpb.c
index e85619e5..728b1f8a 100644
--- a/src/mmhlpb.c
+++ b/src/mmhlpb.c
@@ -1293,11 +1293,10 @@ H("        statement matching <label-match>.  This is useful for avoiding");
 H("        the use of undesired axioms when reducing proof length.  For");
 H("        example, MINIMIZE_WITH ... / FORBID ax-ac,ax-inf* will not shorten");
 H("        the proof with any statement that depends on ax-ac, ax-inf, or");
-H("        ax-inf2 (in the set.mm as of this writing).  Notes: 1. / FORBID");
-H("        can be less useful than / NO_NEW_AXIOMS_FROM because it will");
-H("        also suppress trying statements that depend on <label-list> axioms");
-H("        already used by the proof.  / FORBID may become deprecated.  2. The");
-H("        use of / FORBID without / ALLOW_NEW_AXIOMS has no effect.");
+H("        ax-inf2 (in the set.mm as of this writing).  Note: / FORBID can be");
+H("        less useful than / NO_NEW_AXIOMS_FROM because it will also suppress");
+H("        trying statements that depend on <label-list> axioms already used");
+H("        by the proof.  / FORBID may become deprecated.");
 H("    / OVERRIDE - By default, MINIMIZE_WITH skips statements that have");
 H("        \"(New usage is discouraged.)\" in their description comment.");
 H("        With this qualifier it will try to use them anyway.");