# HG changeset patch
# User blanchet
# Date 1311846225 -7200
# Node ID 5784609715172f071e26cd6bd59bd6e255d859cc
# Parent  4d1270ddf0420bfb8f89d858109e82b2b655319b
fixed lambda concealing

diff -r 4d1270ddf042 -r 578460971517 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 28 11:43:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 28 11:43:45 2011 +0200
@@ -931,12 +931,13 @@
       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   end
 
-fun do_conceal_lambdas Ts (t1 $ t2) =
-    do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
-  | do_conceal_lambdas Ts (Abs (_, T, t)) =
-    (* slightly unsound because of hash collisions *)
-    Free (polymorphic_free_prefix ^ serial_string (), T --> fastype_of1 (Ts, t))
-  | do_conceal_lambdas _ t = t
+fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
+    do_cheaply_conceal_lambdas Ts t1
+    $ do_cheaply_conceal_lambdas Ts t2
+  | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
+    Free (polymorphic_free_prefix ^ serial_string (),
+          T --> fastype_of1 (T :: Ts, t))
+  | do_cheaply_conceal_lambdas _ t = t
 
 fun do_introduce_combinators ctxt Ts t =
   let val thy = Proof_Context.theory_of ctxt in
@@ -947,7 +948,7 @@
       |> reveal_bounds Ts
   end
   (* A type variable of sort "{}" will make abstraction fail. *)
-  handle THM _ => t |> do_conceal_lambdas Ts
+  handle THM _ => t |> do_cheaply_conceal_lambdas Ts
 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
 
 fun preprocess_abstractions_in_terms trans_lambdas facts =