diff -r 4b1a63678839 -r 7943b69f0188 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -1017,7 +1017,7 @@
 
 fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
   let
-    val t' = list_abs_free (Term.add_frees t [], t)
+    val t' = fold_rev absfree (Term.add_frees t []) t
     val options = code_options_of (Proof_Context.theory_of ctxt)
     val thy = Theory.copy (Proof_Context.theory_of ctxt)
     val ((((full_constname, constT), vs'), intro), thy1) =