Lines Matching refs:depth
1165 fun perform_rewrite depth RR term rewrite =
1167 val (hyp_set,_) = (map (map (backchain_rewrite (depth + 1) RR)) ## I)
1178 (apply_rewrite depth RR p))) THENC
1187 and apply_rewrite depth RR conj =
1192 (backchain_rewrite (depth + 1)
1200 UNBOOL_RULE (tryfind_e Empty (backchain_rewrite (depth + 1) RR)
1207 and backchain_rewrite depth RR term =
1208 let val _ = trace 3 ("#" ^ int_to_string depth)
1209 val _ = if depth > !max_depth then raise Empty else ()
1218 (backchain_rewrite depth
1226 then backchain_rewrite depth RR (mk_neg term)
1228 tryfind_e Empty (perform_rewrite depth RR term) quick_ordered handle _ =>
1229 tryfind_e Empty (perform_rewrite depth RR term) slow_ordered