Fix a bug due to ununsed variables

Turn on --warnon:1182 to avoid this mistake in the future.

Put a try/with block around unsafe comparison (which indeed threw
exceptions in some cases).

Down to 7 failing tests.

There are still 38 failing theorems.