# HG changeset patch
# User nipkow
# Date 1118559221 -7200
# Node ID 8af448f67cef95f2ee890818d3fdeeb29a27684c
# Parent  9da1cf997e79a1f4ef2cb8d2459f0178571fb66f
simp_depth now starts at -1 to make it start at 0 ;-)

diff -r 9da1cf997e79 -r 8af448f67cef src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Sat Jun 11 23:24:33 2005 +0200
+++ b/src/Pure/meta_simplifier.ML	Sun Jun 12 08:53:41 2005 +0200
@@ -105,7 +105,7 @@
 
 val debug_simp = ref false;
 val trace_simp = ref false;
-val simp_depth = ref 0;
+val simp_depth = ref (~1);
 val simp_depth_limit = ref 1000;
 val trace_simp_depth_limit = ref 1000;
 
@@ -1102,7 +1102,7 @@
          error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
            Pretty.string_of (Display.pretty_thms thms))
    in simp_depth := !simp_depth - 1; res end
-  ) handle exn => (simp_depth := 0; raise exn);
+  ) handle exn => (simp_depth := !simp_depth - 1; raise exn);
 
 (*Rewrite a cterm*)
 fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)