
diff -r f6e351043014 -r 1e1782c1aedf src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Sat Feb 17 20:03:37 2018 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Sun Feb 18 15:05:21 2018 +0100
@@ -194,7 +194,7 @@
 
 fun subprob_cong thm ctxt = (
   let
-    val thm' = Thm.transfer (Proof_Context.theory_of ctxt) thm
+    val thm' = Thm.transfer' ctxt thm
     val free = thm' |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |>
       dest_comb |> snd |> strip_abs_body |> head_of |> is_Free
   in




