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