[isabelle-dev] HOL-Mutabelle broken

[Makarius]

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