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