# HG changeset patch
# User hoelzl
# Date 1354719528 -3600
# Node ID d00e2b0ca0699f5e50c557d3cf050c239ec1dbee
# Parent  837e38a42d8cb3440a306c6f68054ee4dd5f1e32
Show search depth in the debug output of the measurability prover

diff -r 837e38a42d8c -r d00e2b0ca069 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 05 15:58:45 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 05 15:58:48 2012 +0100
@@ -1702,12 +1702,14 @@
         handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
         handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
 
-    val depth_measurable_tac = REPEAT
-      (COND (is_cond_formula 1)
-        (debug_tac ctxt (K "simp") (SOLVED' (asm_full_simp_tac ss) 1))
-        ((debug_tac ctxt (K "single") (resolve_tac imported_thms 1)) APPEND
+    fun REPEAT_cnt f n st = ((f n THEN REPEAT_cnt f (n + 1)) ORELSE all_tac) st
+
+    val depth_measurable_tac = REPEAT_cnt (fn n =>
+       (COND (is_cond_formula 1)
+        (debug_tac ctxt (K ("simp " ^ string_of_int n)) (SOLVED' (asm_full_simp_tac ss) 1))
+        ((debug_tac ctxt (K ("single " ^ string_of_int n)) (resolve_tac imported_thms 1)) APPEND
           (split_app_tac ctxt 1) APPEND
-          (splitter 1)))
+          (splitter 1)))) 0
 
   in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;