src/HOL/Tools/ATP/atp_translate.ML
changeset 44504 6f29df8d2007
parent 44502 c537d5e5a365
child 44505 2c1fc7b29c9c
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 23:55:21 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 00:05:45 2011 +0200
     1.3 @@ -1889,9 +1889,8 @@
     1.4    let
     1.5      val level = level_of_type_enc type_enc
     1.6      val should_encode = should_encode_type ctxt mono level
     1.7 -    fun add_type T = should_encode T ? insert_type ctxt I T
     1.8 -    fun add_term (tm as IApp (tm1, tm2)) =
     1.9 -        add_type (ityp_of tm) #> add_term tm1 #> add_term tm2
    1.10 +    fun add_type T = not (should_encode T) ? insert_type ctxt I T
    1.11 +    fun add_term (tm as IApp (_, tm2)) = add_type (ityp_of tm) #> add_term tm2
    1.12        | add_term tm = add_type (ityp_of tm)
    1.13    in formula_fold NONE (K add_term) end
    1.14  fun add_fact_monotonic_types ctxt mono type_enc =