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