1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -810,8 +810,9 @@
     1.4  
     1.5  fun test_term ctxt (t, []) =
     1.6    let
     1.7 +    val t' = list_abs_free (Term.add_frees t [], t)
     1.8      val thy = ProofContext.theory_of ctxt;
     1.9 -    val (xs, p) = strip_abs t;
    1.10 +    val (xs, p) = strip_abs t';
    1.11      val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;
    1.12      val args = map Free args';
    1.13      val (ps, q) = strip_imp p;