1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
     1.3 @@ -686,9 +686,11 @@
     1.4  
     1.5  (* Requires bound variables not to clash with any schematic variables (as should
     1.6     be the case right after lambda-lifting). *)
     1.7 -fun open_form (Const (@{const_name All}, _) $ Abs (_, T, t)) =
     1.8 -    subst_bound (Var ((Name.uu ^ Int.toString (size_of_term t), 0), T), t)
     1.9 -    |> open_form
    1.10 +fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) =
    1.11 +    let
    1.12 +      val names = Name.make_context (map fst (Term.add_var_names t []))
    1.13 +      val (s, _) = Name.variant s names
    1.14 +    in open_form (subst_bound (Var ((s, 0), T), t)) end
    1.15    | open_form t = t
    1.16  
    1.17  fun lift_lams_part_1 ctxt type_enc =