diff -r 7fb011dd51de -r 8c20eb9a388d src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:58 2010 +0200
@@ -283,7 +283,7 @@
     val (body, Ts, fp) = HOLogic.strip_psplits split;
     val output_names = Name.variant_list (Term.add_free_names body [])
       (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
-    val output_frees = map2 (curry Free) output_names (rev Ts)
+    val output_frees = rev (map2 (curry Free) output_names Ts)
     val body = subst_bounds (output_frees, body)
     val (pred as Const (name, T), all_args) =
       case strip_comb body of