src/HOL/Probability/measurable.ML
changeset 54883 dd04a8b654fc
parent 53043 8cbfbeb566a4
child 56491 a8ccf3d6a6e4
     1.1 --- a/src/HOL/Probability/measurable.ML	Tue Dec 31 11:19:14 2013 +0100
     1.2 +++ b/src/HOL/Probability/measurable.ML	Tue Dec 31 14:29:16 2013 +0100
     1.3 @@ -153,9 +153,8 @@
     1.4  
     1.5  fun measurable_tac' ctxt facts =
     1.6    let
     1.7 -
     1.8      val imported_thms =
     1.9 -      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
    1.10 +      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf ctxt) facts) @ get_all ctxt
    1.11  
    1.12      fun debug_facts msg () =
    1.13        msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"