src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Aug 31 08:00:55 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Aug 31 08:00:56 2010 +0200
@@ -351,7 +351,7 @@
         |> map (fn (resargs, (names', prems')) =>
           let
             val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
-          in (prem'::prems', names') end)
+          in (prems' @ [prem'], names') end)
       end
     val intro_ts' = folds_map rewrite prems frees
       |> maps (fn (prems', frees') =>