Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing
authorblanchet
Tue, 18 Oct 2011 15:40:59 +0200
changeset 45168 0e8e662013f9
parent 45167 6bc8d260d459
child 45169 4baa475a51e6
freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing
src/HOL/Tools/ATP/atp_translate.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle