simp_depth now starts at -1 to make it start at 0 ;-)
authornipkow
Sun Jun 12 08:53:41 2005 +0200 (2005-06-12)
changeset 163788af448f67cef
parent 16377 9da1cf997e79
child 16379 d29d27e0f59f
simp_depth now starts at -1 to make it start at 0 ;-)
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Sat Jun 11 23:24:33 2005 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Sun Jun 12 08:53:41 2005 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4  
     1.5  val debug_simp = ref false;
     1.6  val trace_simp = ref false;
     1.7 -val simp_depth = ref 0;
     1.8 +val simp_depth = ref (~1);
     1.9  val simp_depth_limit = ref 1000;
    1.10  val trace_simp_depth_limit = ref 1000;
    1.11  
    1.12 @@ -1102,7 +1102,7 @@
    1.13           error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
    1.14             Pretty.string_of (Display.pretty_thms thms))
    1.15     in simp_depth := !simp_depth - 1; res end
    1.16 -  ) handle exn => (simp_depth := 0; raise exn);
    1.17 +  ) handle exn => (simp_depth := !simp_depth - 1; raise exn);
    1.18  
    1.19  (*Rewrite a cterm*)
    1.20  fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)