[isabelle-dev] HOL-Mutabelle broken

[Lukas Bulwahn]

With changeset aa35c9454a95, HOL-Mutabelle compiles again.

Lukas

On 11/09/2011 06:16 PM, Makarius wrote:
> In Isabelle/d17556b9a89b HOL-Mutabelle is broken:
>
> HOL-Mutabelle FAILED
> (see also 
> /Volumes/Macintosh_HD/Users/makarius/.isabelle//heaps/polyml-5.4.2_x86_64-darwin/log/HOL-Mutabelle)
>
> ***       int list -> term list option * Quickcheck.report option
> ***    Reason:
> ***    Can't unify string * Quickcheck_Common.compile_generator to
> ***       Proof.context ->
> ***       (term * term list) list ->
> ***       int list -> term list option * Quickcheck.report option
> ***       (Incompatible types)
> *** Error (line 499 of "~~/src/HOL/Mutabelle/mutabelle.ML"):
> *** Type error in function application.
> ***    Function:
> ***       Quickcheck_Common.test_term
> ***       Exhaustive_Generators.compile_generator_expr
> ***       ctxt'
> ***       : bool -> term * term list -> Quickcheck.result
> ***    Argument: (true, false) : bool * bool
> ***    Reason: Can't unify bool to bool * bool (Incompatible types)
> ***
> *** At command "theory" (line 1 of 
> "~~/src/HOL/Mutabelle/MutabelleExtra.thy") Exception- TOPLEVEL_ERROR 
> raised
> *** ML error
>
> I have tried to repair this myself, but failed to understand the 3-4 
> changesets leading up to that problem -- just too many obscure 
> booleans floating around, and no proper explanations in the changelogs.
>
>
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>