src/HOL/Tools/inductive_codegen.ML
changeset 44241 7943b69f0188
parent 44121 44adaa6db327
child 45159 3f1d1ce024cb
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -871,7 +871,7 @@
 
 fun test_term ctxt [(t, [])] =
       let
-        val t' = list_abs_free (Term.add_frees t [], t)
+        val t' = fold_rev absfree (Term.add_frees t []) t;
         val thy = Proof_Context.theory_of ctxt;
         val (xs, p) = strip_abs t';
         val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;