diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp
index 252bbecd3..81714f697 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -10,7 +10,6 @@
 #include "math/lp/nla_core.h"
 #include "math/lp/nla_common.h"
 #include "math/lp/factorization_factory_imp.h"
-#include "util/trail.h"
 
 namespace nla {
 
diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h
index c300d72c1..401e4eb62 100644
--- a/src/math/lp/nla_types.h
+++ b/src/math/lp/nla_types.h
@@ -66,8 +66,8 @@ namespace nla {
     class core;
     //
     // lemmas are created in a scope.
-    // when the destructor of new_lemma is invoked
-    // all constraints are assumed added to the lemma
+    // when the destructor of lemma_builder is invoked
+    // all constraints are assumed already added to the current_lemma
     // correctness of the lemma can be checked at this point.
     //
     class lemma_builder {