[isabelle-dev] Isabelle/jEdit: non-trivial theory merge

[Lars Noschinski]

Hi,

today (57bf0cecb366) I noticed some strange behaviour in jEdit when 
bootstrapping HOL. I had HOL fully loaded (after working around the 
usual problems with newly defined commands). However, every change which 
causes FunDef.thy to be reprocessed, triggered error in later theories 
using the "fun" or "function" commands:

For example, Divide.thy at line 1194:

   function posDivAlg :: "int ⇒ int ⇒ int × int" where
     "posDivAlg a b = (if a < b ∨  b ≤ 0 then (0, a)
        else adjust b (posDivAlg a (2 * b)))"

with

   Attempt to perform non-trivial merge of theories:
   {..., Relation, Transitive_Closure, Partial_Function, Wellfounded, 
FunDef:33}
   {..., Equiv_Relations, Int, Nat_Numeral, Nat_Transfer, Divides:408}

When I reload Divide.thy, this problem goes away. Similar problems occur 
at other uses of "function" in later theories.

I recall that I was able to do changes in early HOL without such 
problems with jEdit some months ago.

   -- Lars