Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Mon, 27 Jul 2015 23:56:11 +0200
changeset 60807 d7e6c7760db5
parent 60806 622d45ca75ee
child 60808 fd26519b1a6a
tuned;
src/HOL/Probability/measurable.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle