--- a/src/HOL/Tools/ATP/atp_translate.ML Fri Aug 26 00:19:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Aug 26 01:14:49 2011 +0200
@@ -1889,8 +1889,9 @@
val level = level_of_type_enc type_enc
val should_encode = should_encode_type ctxt mono level
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)
+ fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
+ | add_args _ = I
+ and add_term tm = add_type (ityp_of tm) #> add_args tm
in formula_fold NONE (K add_term) end
fun add_fact_monotonic_types ctxt mono type_enc =
add_iformula_monotonic_types ctxt mono type_enc |> fact_lift