diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean
index 18b90888eb58..7f5800c2d7db 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean
@@ -59,8 +59,7 @@ partial def structuresPass : Pass where
         return false
       else
         let some const := decl.type.getAppFn.constName? | return false
-        let some ofInterest := interesting.get? const | return false
-        return ofInterest
+        return interesting.getD const false
     match goals with
     | [goal] => return goal
     | _ => throwError "structures preprocessor generated more than 1 goal"