# HG changeset patch
# User boehmes
# Date 1256898694 -3600
# Node ID ee5b5ef5e970abcdf3d14dc0ea6130499824b97c
# Parent  1f70087cdef5a93c980f246daa010adb9057f33b
abstract over variables in reversed order (application uses given order)

diff -r 1f70087cdef5 -r ee5b5ef5e970 src/HOL/SMT/Tools/smt_normalize.ML
--- a/src/HOL/SMT/Tools/smt_normalize.ML	Fri Oct 30 11:27:47 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Fri Oct 30 11:31:34 2009 +0100
@@ -318,7 +318,7 @@
   fun replace ctxt cvs ct (cx as (nctxt, defs)) =
     let
       val cvs' = used_vars cvs ct
-      val ct' = fold Thm.cabs cvs' ct
+      val ct' = fold_rev Thm.cabs cvs' ct
       val mk_repl = fold (fn ct => fn cu => Thm.capply cu ct) cvs'
     in
       (case Termtab.lookup defs (Thm.term_of ct') of