Fix discouraged check

tirix · Jan 30, 2024 · 21133bb · 21133bb
1 parent 516d58f
commit 21133bb
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/metamath-knife/src/main.rs b/metamath-knife/src/main.rs
@@ -251,7 +251,6 @@ fn main() {
         }
 
         if let Some(exps) = matches.values_of_lossy("minimize") {
-            db.name_pass();
             db.stmt_parse_pass();
             for label in exps {
                 minimize(&db, &label);

diff --git a/metamath-knife/src/minimizer.rs b/metamath-knife/src/minimizer.rs
@@ -92,7 +92,7 @@ pub fn minimize(db: &Database, label_str: &str) {
     let provable_typecode = db.grammar_result().provable_typecode();
     for theorem in db
         .statements_range(..label)
-        .filter(|s| s.is_assertion() && !sref.discouragements().usage_discouraged)
+        .filter(|s| s.is_assertion() && !s.discouragements().usage_discouraged)
     {
         let formula = db.stmt_parse_result().get_formula(&theorem).unwrap();
         if formula.get_typecode() == provable_typecode {