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

Hi Lars,

note that this is not specific to datatypes, but rather the general simplifier setup seems to be really messed up with this order of imports.

Try e.g.,

theory B
 imports A Main
lemma "x = y â y = x"
  by simp (* Failed to apply initial proof method *)

fun f where (*Tactic failed*)
  "f x = x"



> On 13 Feb 2017, at 17:09, Lars Hupel <hupel at> wrote:
> 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.