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;