[isabelle-dev] HOL-Codegenerator_Test and scala-2.10.0-M2

[Makarius]

We are officially still on stable scala-2.9.2, but the Scala guys are 
moving slowly towards scala-2.10.0, so it is worth testing that aready.

Doing this with Isabelle/8d2251b9a200, it causes HOL-Codegenerator_Test
to fail like this:

HOL-Codegenerator_Test FAILED
(see also 
/Volumes/Macintosh_HD/Users/makarius/.isabelle/heaps/polyml-5.5.0_x86-darwin/log/HOL-Codegenerator_Test)

   case (FunBox(funa), FunBox(fun)) => eq[A => B](funa, fun)
                                                        ^
ROOT.scala:10445: error: type mismatch;
  found   : ?A2447 => (B, C) where type ?A2447 <: A (this is a GADT skolem)
  required: A => (B, C)
   case (f1, Tuple_Isomorphism(fun1, fun2)) => (f1(fun1))(fun2)
                                                   ^
ROOT.scala:10695: error: type mismatch;
  found   : ?A2492 => (B, C) where type ?A2492 <: A (this is a GADT skolem)
  required: A => (B, C)
     eq[A => (B, C)](fun1a, fun1) && eq[((B, C)) => A](fun2a, fun2)

etc.


There are documents on http://www.scala-lang.org such as 
http://www.scala-lang.org/node/16606 that explain the quite substantial 
reforms of Scala that Odersky is rolling out in the coming release.


 	Makarius