Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Probability/Probability_Measure.thy
changeset 61125 4c68426800de
parent 59427 084330e2ec5e
child 61169 4de9ff3ea29a 
--- a/src/HOL/Probability/Probability_Measure.thy	Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Sun Sep 06 22:14:51 2015 +0200
@@ -278,7 +278,7 @@
             in
               go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
             end
-        | go pattern elem (Const (@{const_syntax case_prod}, _) $ t) =
+        | go pattern elem (Const (@{const_syntax uncurry}, _) $ t) =
             go 
               ((Syntax.const @{syntax_const "_pattern"}, 2) :: pattern)
               (Syntax.const @{const_syntax Pair} :: elem)
isabelle