--- a/src/HOL/Probability/Giry_Monad.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Wed Mar 04 19:53:18 2015 +0100
@@ -184,7 +184,7 @@
fun subprob_cong thm ctxt = (
let
val thm' = Thm.transfer (Proof_Context.theory_of ctxt) thm
- val free = thm' |> concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |>
+ val free = thm' |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |>
dest_comb |> snd |> strip_abs_body |> head_of |> is_Free
in
if free then ([], Measurable.add_local_cong (thm' RS @{thm subprob_measurableD(2)}) ctxt)