[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

    datatype 'a test = Test


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


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