1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Apr 24 09:47:40 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Apr 24 09:47:40 2012 +0200
     1.3 @@ -764,18 +764,6 @@
     1.4      (if String.isPrefix lam_lifted_prefix s then Const else Free) x
     1.5    | constify_lifted t = t
     1.6  
     1.7 -(* Requires bound variables not to clash with any schematic variables (as should
     1.8 -   be the case right after lambda-lifting). *)
     1.9 -fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) =
    1.10 -    (case try unprefix s of
    1.11 -       SOME s =>
    1.12 -       let
    1.13 -         val names = Name.make_context (map fst (Term.add_var_names t' []))
    1.14 -         val (s, _) = Name.variant s names
    1.15 -       in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end
    1.16 -     | NONE => t)
    1.17 -  | open_form _ t = t
    1.18 -
    1.19  fun lift_lams_part_1 ctxt type_enc =
    1.20    map close_form #> rpair ctxt
    1.21    #-> Lambda_Lifting.lift_lambdas
    1.22 @@ -792,6 +780,8 @@
    1.23       of them *)
    1.24    |> pairself (map (introduce_combinators ctxt))
    1.25    |> pairself (map constify_lifted)
    1.26 +  (* Requires bound variables not to clash with any schematic variables (as
    1.27 +     should be the case right after lambda-lifting). *)
    1.28    |>> map (open_form (unprefix close_form_prefix))
    1.29    ||> map (open_form I)
    1.30