The translator accepts constants with preconditions

[oskarabrahamsson]

The translator accepts constants with preconditions, and duplicates preconditions:

> val foo_def = Define` foo = 5 DIV 0`;

Definition has been stored under "foo_def"
val foo_def =  [] ⊢ foo = 5 DIV 0: thm

> val th = translate foo_def;

Translating foo

WARNING: foo has a precondition.

val th =  [foo_side, PRECONDITION foo_side] ⊢ NUM foo foo_v: thm

What's worse, the precondition also leaks into the theorem produced by ml_progLib:

> get_ml_prog_state() |> ml_progLib.get_thm;
val it =  [foo_side] ⊢ ... ... [... ] (scratch_st ffi): thm