[isabelle] Theory merge in wrong order leads to error in datatype



Dear list,

assume you have two files:

  theory A
  imports Pure
  begin (* empty *) end

  theory B
  imports A Main
  begin

    datatype 'a test = Test

  end

The "datatype" command produces a tactic failure, with the exception
"Congruence not a meta-equality".

If I swap the order of imports, the problem goes away.

I'm aware that changing the order of imports might influence qualified
names, but I haven't observed anything like that before. The above
example throws an error in 2016-1 (and 49c537d87896), but succeeds in
Isabelle2016.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.