Wrong error messages for definitions with mismatched proofs

[sankalpgambhir]

Consider the following theorem and definition which do not correspond to each other:

  val testThm = makeTHM("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") {
    val i1 = have(P(x) ==> P(f(x)) |- P(x) ==> P(f(x))) by Restate;
  }
  show

  val testdef = DEF (x) --> The(y, (y === x))(testThm)

We expect an error saying the provided theorem does not justify the definition. However, instead you get a complaint about free variables:

[info] running Exercise 
 Theorem testThm := 'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))

   Definition of testdef at.(Exercise.scala:18) is invalid:
   val testdef = DEF (x) --> The(y, (y === x))(testThm)

   The definition is not allowed to contain schematic symbols or free variables.The symbols {VariableLabel(y)} are free in the expression 'y = 'x.