--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Feb 10 16:33:58 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Feb 10 17:10:47 2012 +0100
@@ -2711,6 +2711,8 @@
(s, args)
| have_head_rolling _ = ("", [])
+val max_kbo_weight = 2147483647
+
fun atp_problem_kbo_weights problem =
let
fun add_term_deps head (ATerm (s, args)) =
@@ -2735,7 +2737,7 @@
val graph =
Graph.empty |> fold (fold (add_line_deps spec_eqN) o snd) problem
|> fold (fold (add_line_deps simpN) o snd) problem
- fun next_weight w = w + w
+ fun next_weight w = if w + w <= max_kbo_weight then w + w else w + 1
fun add_weights _ [] = I
| add_weights weight syms =
fold (AList.update (op =) o rpair weight) syms