# HG changeset patch
# User blanchet
# Date 1314309945 -7200
# Node ID 6f29df8d20077de822f31c14edc23c9c783c174b
# Parent  97ec9abd3253df2e590e3d9370d10c280e8a3dea
fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings

diff -r 97ec9abd3253 -r 6f29df8d2007 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 23:55:21 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 00:05:45 2011 +0200
@@ -1889,9 +1889,8 @@
   let
     val level = level_of_type_enc type_enc
     val should_encode = should_encode_type ctxt mono level
-    fun add_type T = should_encode T ? insert_type ctxt I T
-    fun add_term (tm as IApp (tm1, tm2)) =
-        add_type (ityp_of tm) #> add_term tm1 #> add_term tm2
+    fun add_type T = not (should_encode T) ? insert_type ctxt I T
+    fun add_term (tm as IApp (_, tm2)) = add_type (ityp_of tm) #> add_term tm2
       | add_term tm = add_type (ityp_of tm)
   in formula_fold NONE (K add_term) end
 fun add_fact_monotonic_types ctxt mono type_enc =