1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 28 11:43:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 28 11:43:45 2011 +0200
     1.3 @@ -931,12 +931,13 @@
     1.4        in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
     1.5    end
     1.6  
     1.7 -fun do_conceal_lambdas Ts (t1 $ t2) =
     1.8 -    do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
     1.9 -  | do_conceal_lambdas Ts (Abs (_, T, t)) =
    1.10 -    (* slightly unsound because of hash collisions *)
    1.11 -    Free (polymorphic_free_prefix ^ serial_string (), T --> fastype_of1 (Ts, t))
    1.12 -  | do_conceal_lambdas _ t = t
    1.13 +fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
    1.14 +    do_cheaply_conceal_lambdas Ts t1
    1.15 +    $ do_cheaply_conceal_lambdas Ts t2
    1.16 +  | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
    1.17 +    Free (polymorphic_free_prefix ^ serial_string (),
    1.18 +          T --> fastype_of1 (T :: Ts, t))
    1.19 +  | do_cheaply_conceal_lambdas _ t = t
    1.20  
    1.21  fun do_introduce_combinators ctxt Ts t =
    1.22    let val thy = Proof_Context.theory_of ctxt in
    1.23 @@ -947,7 +948,7 @@
    1.24        |> reveal_bounds Ts
    1.25    end
    1.26    (* A type variable of sort "{}" will make abstraction fail. *)
    1.27 -  handle THM _ => t |> do_conceal_lambdas Ts
    1.28 +  handle THM _ => t |> do_cheaply_conceal_lambdas Ts
    1.29  val introduce_combinators = simple_translate_lambdas do_introduce_combinators
    1.30  
    1.31  fun preprocess_abstractions_in_terms trans_lambdas facts =