# HG changeset patch # User wenzelm # Date 1438034171 -7200 # Node ID d7e6c7760db5eab0d615032b5a24a4e78fdbf7eb # Parent 622d45ca75ee75d4f6e85299dece437cefcad634 tuned; diff -r 622d45ca75ee -r d7e6c7760db5 src/HOL/Probability/measurable.ML --- a/src/HOL/Probability/measurable.ML Mon Jul 27 23:41:57 2015 +0200 +++ b/src/HOL/Probability/measurable.ML Mon Jul 27 23:56:11 2015 +0200 @@ -250,9 +250,10 @@ Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) => let val f = dest_measurable_fun (HOLogic.dest_Trueprop t) - fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt))) fun inst (ts, Ts) = - Thm.instantiate' (cert Thm.global_ctyp_of Ts) (cert Thm.global_cterm_of ts) + Thm.instantiate' + (map (Option.map (Thm.ctyp_of ctxt)) Ts) + (map (Option.map (Thm.cterm_of ctxt)) ts) @{thm measurable_compose_countable} in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end handle TERM _ => no_tac) 1)