[isabelle-dev] HOL-Probability broken

[Makarius]

In Isabelle/cd945dc13bec HOL-Probability is broken:

*** Now trying to infer coercions globally.
***
*** Coercion inference failed:
*** uncomparable types in type list
***
*** Cannot fulfil subtype constraints:
***   ??'a  <:  ereal   from function application
***     \<integral>\<^sup>+ x. ereal (x ^ k * exp (- x)) *
***                            indicator {0::??'i..} x
***                        \<partial>lborel =
***     fact k
***   ereal  <:  ereal   from function application
***     op =
***      (\<integral>\<^sup>+ x. ereal (x ^ k * exp (- x)) *
***                              indicator {0::??'h..} x
***                          \<partial>lborel)
***   nat => ??'a  <:  ??'b => ??'c   from function application
***     fact::??'b => ??'c
*** At command "lemma" (line 116 of "~~/src/HOL/Probability/Distributions.thy")

The problem might be an untested merge by Larry, but I did not make more 
detailed tests to prove that hypothesis.

What is also odd: http://isabelle.in.tum.de/reports/Isabelle does not show 
any activity nor results of testing.  Maybe the mira service is down?


 	Makarius