src/HOL/Probability/Giry_Monad.thy
changeset 67649 1e1782c1aedf
parent 67399 eab6ce8368fa
child 69260 0a9688695a1b
--- 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