# HG changeset patch
# User blanchet
# Date 1311276550 -7200
# Node ID 081718c0b0a86dc08e9248cd27055b7ab531f4ee
# Parent  78a0a2ad91a387d9f1ab5d09f1a5f42e722c0c46
make "concealed" lambda translation sound

diff -r 78a0a2ad91a3 -r 081718c0b0a8 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 21 08:33:57 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jul 21 21:29:10 2011 +0200
@@ -88,7 +88,6 @@
   val unmangled_const_name : string -> string
   val helper_table : ((string * bool) * thm list) list
   val factsN : string
-  val conceal_lambdas : Proof.context -> term -> term
   val introduce_combinators : Proof.context -> term -> term
   val prepare_atp_problem :
     Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
@@ -161,8 +160,6 @@
 (* Freshness almost guaranteed! *)
 val atp_weak_prefix = "ATP:"
 
-val concealed_lambda_prefix = atp_weak_prefix ^ "lambda_"
-
 (*Escaping of special characters.
   Alphanumeric characters are left unchanged.
   The character _ goes to __
@@ -926,10 +923,8 @@
     do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
   | do_conceal_lambdas Ts (Abs (_, T, t)) =
     (* slightly unsound because of hash collisions *)
-    Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
-          T --> fastype_of1 (Ts, t))
+    Free (polymorphic_free_prefix ^ serial_string (), T --> fastype_of1 (Ts, t))
   | do_conceal_lambdas _ t = t
-val conceal_lambdas = simple_translate_lambdas (K do_conceal_lambdas)
 
 fun do_introduce_combinators ctxt Ts t =
   let val thy = Proof_Context.theory_of ctxt in
diff -r 78a0a2ad91a3 -r 081718c0b0a8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 21 08:33:57 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 21 21:29:10 2011 +0200
@@ -525,6 +525,12 @@
    | NONE => type_enc_from_string best_type_enc)
   |> choose_format formats
 
+fun lift_lambdas ctxt =
+  map (close_form o Envir.eta_contract) #> rpair ctxt
+  #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix)
+                                  Lambda_Lifting.is_quantifier
+  #> fst
+
 fun translate_atp_lambdas ctxt type_enc =
   Config.get ctxt atp_lambda_translation
   |> (fn trans =>
@@ -538,16 +544,13 @@
            trans)
   |> (fn trans =>
          if trans = concealedN then
-           rpair [] o map (conceal_lambdas ctxt)
+           lift_lambdas ctxt ##> K []
          else if trans = liftingN then
-           map (close_form o Envir.eta_contract) #> rpair ctxt
-           #-> Lambda_Lifting.lift_lambdas (SOME polymorphic_free_prefix)
-                                           Lambda_Lifting.is_quantifier
-           #> fst
+           lift_lambdas ctxt
          else if trans = combinatorsN then
-           rpair [] o map (introduce_combinators ctxt)
+           map (introduce_combinators ctxt) #> rpair []
          else if trans = lambdasN then
-           rpair [] o map (Envir.eta_contract)
+           map (Envir.eta_contract) #> rpair []
          else
            error ("Unknown lambda translation method: " ^ quote trans ^ "."))