1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -1909,8 +1909,18 @@
     1.4    |> ho_term_from_iterm ctxt format mono type_enc pos
     1.5    |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
     1.6         | _ => raise Fail "unexpected lambda-abstraction")
     1.7 -and ho_term_from_iterm ctxt format mono type_enc =
     1.8 +and ho_term_from_iterm ctxt format mono type_enc pos =
     1.9    let
    1.10 +    fun beta_red bs (IApp (IAbs ((name, _), tm), tm')) =
    1.11 +        beta_red ((name, beta_red bs tm') :: bs) tm
    1.12 +      | beta_red bs (IApp tmp) = IApp (pairself (beta_red bs) tmp)
    1.13 +      | beta_red bs (tm as IConst (name, _, _)) =
    1.14 +        (case AList.lookup (op =) bs name of
    1.15 +           SOME tm' => tm'
    1.16 +         | NONE => tm)
    1.17 +      | beta_red bs (IAbs ((name, T), tm)) =
    1.18 +        IAbs ((name, T), beta_red (AList.delete (op =) name bs) tm)
    1.19 +      | beta_red _ tm = tm
    1.20      fun term site u =
    1.21        let
    1.22          val (head, args) = strip_iterm_comb u
    1.23 @@ -1922,7 +1932,9 @@
    1.24          val t =
    1.25            case head of
    1.26              IConst (name as (s, _), _, T_args) =>
    1.27 -            let val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere in
    1.28 +            let
    1.29 +              val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
    1.30 +            in
    1.31                map (term arg_site) args |> mk_aterm format type_enc name T_args
    1.32              end
    1.33            | IVar (name, _) =>
    1.34 @@ -1941,7 +1953,7 @@
    1.35          else
    1.36            t
    1.37        end
    1.38 -  in term o Top_Level end
    1.39 +  in term (Top_Level pos) o beta_red [] end
    1.40  and formula_from_iformula ctxt polym_constrs format mono type_enc
    1.41                            should_guard_var =
    1.42    let