src/HOL/Tools/ATP/atp_translate.ML
changeset 44506 7e3913e70846
parent 44505 2c1fc7b29c9c
child 44508 5438d88b2cb7
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 00:19:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 01:14:49 2011 +0200
     1.3 @@ -1889,8 +1889,9 @@
     1.4      val level = level_of_type_enc type_enc
     1.5      val should_encode = should_encode_type ctxt mono level
     1.6      fun add_type T = not (should_encode T) ? insert_type ctxt I T
     1.7 -    fun add_term (tm as IApp (_, tm2)) = add_type (ityp_of tm) #> add_term tm2
     1.8 -      | add_term tm = add_type (ityp_of tm)
     1.9 +    fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
    1.10 +      | add_args _ = I
    1.11 +    and add_term tm = add_type (ityp_of tm) #> add_args tm
    1.12    in formula_fold NONE (K add_term) end
    1.13  fun add_fact_monotonic_types ctxt mono type_enc =
    1.14    add_iformula_monotonic_types ctxt mono type_enc |> fact_lift