src/HOL/Probability/measurable.ML
changeset 56491 a8ccf3d6a6e4
parent 54883 dd04a8b654fc
child 58965 a62cdcc5344b
     1.1 --- a/src/HOL/Probability/measurable.ML	Wed Apr 09 11:32:41 2014 +0200
     1.2 +++ b/src/HOL/Probability/measurable.ML	Wed Apr 09 12:22:57 2014 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5  fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
     1.6  
     1.7 -fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
     1.8 +fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
     1.9  
    1.10  fun nth_hol_goal thm i =
    1.11    HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))