src/HOL/Probability/measurable.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59837 57820650bd11
     1.1 --- a/src/HOL/Probability/measurable.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Probability/measurable.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -251,7 +251,7 @@
     1.4            val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
     1.5            fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
     1.6            fun inst (ts, Ts) =
     1.7 -            Drule.instantiate' (cert Thm.ctyp_of Ts) (cert Thm.cterm_of ts)
     1.8 +            Drule.instantiate' (cert Thm.global_ctyp_of Ts) (cert Thm.global_cterm_of ts)
     1.9                @{thm measurable_compose_countable}
    1.10          in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end
    1.11          handle TERM _ => no_tac) 1)