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.
append instead of prepend lambda-lifted definitions -- this eases reconstruction in veriT (outside repository)
authorblanchet
Thu, 10 Jul 2014 17:01:23 +0200
changeset 57540 10e7aabe1762
parent 57539 353fd3326835
child 57541 147e3f1e0459
append instead of prepend lambda-lifted definitions -- this eases reconstruction in veriT (outside repository)
src/HOL/Tools/SMT2/smt2_translate.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jul 10 14:12:16 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jul 10 17:01:23 2014 +0200
@@ -505,7 +505,7 @@
       |> rpair ctxt1
       |-> Lambda_Lifting.lift_lambdas NONE is_binder
       |-> (fn (ts', defs) => fn ctxt' =>
-          map mk_trigger defs @ ts'
+          ts' @ map mk_trigger defs
           |> intro_explicit_application ctxt' funcs
           |> pair ctxt')
isabelle