diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h
index d13f588e8..fb9c469a8 100644
--- a/src/math/lp/nla_monotone_lemmas.h
+++ b/src/math/lp/nla_monotone_lemmas.h
@@ -7,16 +7,14 @@
   --*/
 #pragma once
 namespace nla {
-class core;
-class monotone : common {    
-public:
-    monotone(core *core);
-    void monotonicity_lemma();
-private:
-    void monotonicity_lemma(monic const& m);
-    void monotonicity_lemma_gt(const monic& m);    
-    void monotonicity_lemma_lt(const monic& m);
-    std::vector<rational> get_sorted_key(const monic& rm) const;
-    vector<std::pair<rational, lpvar>> get_sorted_key_with_rvars(const monic& a) const;
-};
+    class core;
+    class monotone : common {    
+    public:
+        monotone(core *core);
+        void monotonicity_lemma();
+    private:
+        void monotonicity_lemma(monic const& m);
+        void monotonicity_lemma_gt(const monic& m);    
+        void monotonicity_lemma_lt(const monic& m);
+    };
 }