--- a/Nominal/nominal_inductive.ML	Thu Aug 18 14:10:52 2011 +0200
+++ b/Nominal/nominal_inductive.ML	Fri Aug 19 10:56:12 2011 +0900
@@ -104,7 +104,7 @@
       |> map (add_c_prop true Ps (Bound 0, c_name, c_ty))
 
     val avoid_trm' = avoid_trm
-      |> (curry list_abs_free) (params @ [(c_name, c_ty)])
+      |> fold_rev absfree (params @ [(c_name, c_ty)])
       |> strip_abs_body
       |> (fn t => mk_fresh_star_ty c_ty t (Bound 0))
       |> HOLogic.mk_Trueprop
@@ -439,4 +439,4 @@
       Keyword.thy_goal (main_parser >> prove_strong_inductive_cmd)
 end
 
-end
\ No newline at end of file
+end