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/measurable.ML
changeset 54883 dd04a8b654fc
parent 53043 8cbfbeb566a4
child 56491 a8ccf3d6a6e4 
--- a/src/HOL/Probability/measurable.ML	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Probability/measurable.ML	Tue Dec 31 14:29:16 2013 +0100
@@ -153,9 +153,8 @@
 
 fun measurable_tac' ctxt facts =
   let
-
     val imported_thms =
-      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
+      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf ctxt) facts) @ get_all ctxt
 
     fun debug_facts msg () =
       msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
isabelle