# HG changeset patch
# User blanchet
# Date 1405004483 -7200
# Node ID 10e7aabe17620ed365ab084fe93d52a412bd8532
# Parent  353fd33268353f8ecdecd68c709d2f7d92b9212d
append instead of prepend lambda-lifted definitions -- this eases reconstruction in veriT (outside repository)

diff -r 353fd3326835 -r 10e7aabe1762 src/HOL/Tools/SMT2/smt2_translate.ML
--- 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')