# HG changeset patch
# User blanchet
# Date 1340034606 -7200
# Node ID 1a6d5cc6693137c82ccda60a9ebebc4503b9eccb
# Parent  9ed089bcad934731b6534a2aff80757fc4284bea
removed dead code

diff -r 9ed089bcad93 -r 1a6d5cc66931 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jun 18 15:48:43 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jun 18 17:50:06 2012 +0200
@@ -1339,8 +1339,6 @@
 
 type monotonicity_info =
   {maybe_finite_Ts : typ list,
-   surely_finite_Ts : typ list,
-   maybe_infinite_Ts : typ list,
    surely_infinite_Ts : typ list,
    maybe_nonmono_Ts : typ list}
 
@@ -2228,8 +2226,6 @@
 (* We add "bool" in case the helper "True_or_False" is included later. *)
 fun default_mono level =
   {maybe_finite_Ts = [@{typ bool}],
-   surely_finite_Ts = [@{typ bool}],
-   maybe_infinite_Ts = known_infinite_types,
    surely_infinite_Ts =
      case level of
        Nonmono_Types (Strict, _) => []
@@ -2241,8 +2237,7 @@
 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
   | add_iterm_mononotonicity_info ctxt level _
         (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
-        (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
-                  surely_infinite_Ts, maybe_nonmono_Ts}) =
+        (mono as {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts}) =
     let val thy = Proof_Context.theory_of ctxt in
       if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
         case level of
@@ -2253,14 +2248,10 @@
           else if is_type_kind_of_surely_infinite ctxt strictness
                                                   surely_infinite_Ts T then
             {maybe_finite_Ts = maybe_finite_Ts,
-             surely_finite_Ts = surely_finite_Ts,
-             maybe_infinite_Ts = maybe_infinite_Ts,
              surely_infinite_Ts = surely_infinite_Ts |> insert_type thy I T,
              maybe_nonmono_Ts = maybe_nonmono_Ts}
           else
             {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv thy) T,
-             surely_finite_Ts = surely_finite_Ts,
-             maybe_infinite_Ts = maybe_infinite_Ts,
              surely_infinite_Ts = surely_infinite_Ts,
              maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
         | _ => mono