[isabelle] Code equations for UNION in Isabelle2012-RC1



Hi all,

I tried to test the code generator setup for sets in Isabelle2012-RC1. The following test fails although I would have expected it to work. Moreover, I neither understand the error message, nor do I have any idea how to fix the problem.

theory Scratch imports Main begin
export_code UNION in SML file -

*** Type
*** 'a::type set => ('a::type => 'b::type set) => 'b::type set
*** of constant "Complete_Lattices.complete_lattice_class.SUPR"
*** is too specific compared to declared type
*** ?'b::{} set => (?'b::{} => ?'a::{}) => ?'a::{}
*** At command "export_code"

Best regards,
Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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