[isabelle] Porting trouble: Interpretation of locale semiring_1



I'm currently converting theories from 2008 -> 2009:

I'm using the following definition of conc:
RegSet.conc_def: conc ?A ?B = {xs @ ys |xs ys. xs \<in> ?A \<and> ys
\<in> ?B}

Then I do:
  interpretation lc_monoid: monoid_mult "{[]}" conc [...]

  text {* Languages with concatenation (*) and union (+) form a semiring
    with 1-element @{term "{[]}"} and 0-element @{term "{}"}: *}
  interpretation regset_semiring: semiring_1 "{[]}" conc "{}" "op \<union>"
    apply (unfold_locales)
    apply (auto simp add: conc_def)
    done

And get the following error upon the "done" command, i.e. after (!) it
told me "No  subgoals".

*** Partially applied constant on left hand side of equation
*** "semiring_1.of_nat {[]} {} op \<union> ?n \<equiv>
semiring_1.of_nat_aux (\<lambda>i. i \<union> {[]}) ?n {}"
*** At command "done".

I do not know what this error message means, nor can I find any
documentation.
In Isabelle2008, the proof worked well.

Many thanks for any hints,
  Peter







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