# HG changeset patch
# User blanchet
# Date 1318945259 -7200
# Node ID 0e8e662013f919532b47a7d97415ab07ec0c537c
# Parent  6bc8d260d459296e7735d95c5e45a6e8dcf175c6
freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing

diff -r 6bc8d260d459 -r 0e8e662013f9 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Oct 18 15:40:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Oct 18 15:40:59 2011 +0200
@@ -1654,6 +1654,7 @@
     val facts = facts |> map (apsnd (pair Axiom))
     val conjs =
       map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
+      |> map (apsnd freeze_term)
       |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
     val ((conjs, facts), lambdas) =
       if preproc then
@@ -1661,7 +1662,6 @@
         |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
         |> preprocess_abstractions_in_terms trans_lambdas
         |>> chop (length conjs)
-        |>> apfst (map (apsnd (apsnd freeze_term)))
       else
         ((conjs, facts), [])
     val conjs = conjs |> make_conjecture ctxt format type_enc