[isabelle] Porting to 2009: Duplicate facts on locale interpretation



I get a "duplicate fact"-error error when trying to interpret a locale
that imports a fact with the same name from different locales:
In Isabelle2007 this worked well, and I frequently use it. Do I have to
rename all those lemmas to make their names unique, or
is there a simpler way to convert ?

Here follows a toy-example that illustrates the problem:

  locale B =
    assumes Y: "True"
  begin
    lemma A: True ..
  end

  locale C =
    assumes Z: "True"
  begin
    lemma A: True ..
  end

  locale D = B + C
  begin
    lemma A: "True" ..
  end

  interpretation x: D
    apply (unfold_locales)
    apply simp
    done

*** Duplicate fact "Scratch.x.A"
*** At command "done".

Many thanks for any hints,
  Peter








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