# HG changeset patch
# User blanchet
# Date 1328890247 -3600
# Node ID 7560930b2e06105324eadfb8613ade6a51ed006e
# Parent  312b49fba3574a98c962c5c3406804b49e8e8765
be more gentle when generating KBO weights

diff -r 312b49fba357 -r 7560930b2e06 src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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