diff --git a/src/library/norm_num.cpp b/src/library/norm_num.cpp
index 1088b0b2b..ab3da75e2 100644
--- a/src/library/norm_num.cpp
+++ b/src/library/norm_num.cpp
@@ -344,7 +344,6 @@ pair<expr, expr> norm_num_context::mk_norm_mul(expr const & lhs, expr const & rh
         rv = mk_app({rhs_head, type, typec, mtp.first});
         prf = mk_app({mk_const(*g_mul_bit0), type, mk_has_distrib(typec), lhs, args_rhs[2], mtp.first, mtp.second});
     } else if (is_bit1(rhs)) {
-      std::cout << "is_bit1 " << rhs << "\n";
         auto mtp = mk_norm_mul(lhs, args_rhs[3]);
         auto atp = mk_norm_add(mk_app({mk_const(*g_bit0), type, args_rhs[2], mtp.first}), lhs);
 	rv = atp.first;
diff --git a/src/library/tactic/norm_num_tactic.cpp b/src/library/tactic/norm_num_tactic.cpp
index bffcc0947..9e8ac164f 100644
--- a/src/library/tactic/norm_num_tactic.cpp
+++ b/src/library/tactic/norm_num_tactic.cpp
@@ -33,18 +33,17 @@ tactic norm_num_tactic() {
             g.get_hyps(hyps);
             local_context ctx(to_list(hyps));
             try {
-	        //bool bs = is_numeral(env, lhs);
                 pair<expr, expr> p = mk_norm_num(env, ctx, lhs);
                 expr new_lhs = p.first;
                 expr new_lhs_pr  = p.second;
 		pair<expr, expr> p2 = mk_norm_num(env, ctx, rhs);
 		expr new_rhs = p2.first;
 		expr new_rhs_pr = p2.second;
-                //if (new_lhs != new_rhs) {
-		//    std::cout << "lhs: " << new_lhs << ", rhs: " << new_rhs << "\n";
-		//    throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs normal form doesn't match rhs");
-		    //    return none_proof_state();
-		    //}
+                /*if (new_lhs != new_rhs) {
+		    std::cout << "lhs: " << new_lhs << ", rhs: " << new_rhs << "\n";
+		    throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs normal form doesn't match rhs");
+		    return none_proof_state();
+		}*/
 		type_checker tc(env);
 		expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr));
                 substitution new_subst = s.get_subst();