equal
deleted
inserted
replaced
191 |
191 |
192 fun incr_depth(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) = |
192 fun incr_depth(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) = |
193 let val depth1 = depth+1 |
193 let val depth1 = depth+1 |
194 in if depth1 > !simp_depth_limit |
194 in if depth1 > !simp_depth_limit |
195 then (warning "simp_depth_limit exceeded - giving up"; None) |
195 then (warning "simp_depth_limit exceeded - giving up"; None) |
196 else (if depth1 mod 5 = 0 |
196 else (if depth1 mod 10 = 0 |
197 then warning("Simplification depth " ^ string_of_int depth1) |
197 then warning("Simplification depth " ^ string_of_int depth1) |
198 else (); |
198 else (); |
199 Some(mk_mss(rules,congs,procs,bounds,prems,mk_rews,termless,depth1)) |
199 Some(mk_mss(rules,congs,procs,bounds,prems,mk_rews,termless,depth1)) |
200 ) |
200 ) |
201 end; |
201 end; |