--- a/Nominal/nominal_inductive.ML	Mon Jan 09 10:45:12 2012 +0000
+++ b/Nominal/nominal_inductive.ML	Mon Jan 16 12:42:47 2012 +0000
@@ -46,12 +46,12 @@
       |> mk_fresh_star avoid_trm 
       |> HOLogic.mk_Trueprop
       |> (curry Logic.list_implies) prems
-      |> (curry list_all_free) params
+      |> fold_rev (Logic.all o Free) params
     val finite_goal = avoid_trm
       |> mk_finite
       |> HOLogic.mk_Trueprop
       |> (curry Logic.list_implies) prems
-      |> (curry list_all_free) params
+      |> fold_rev (Logic.all o Free) params
   in 
     if null avoid then [] else [vc_goal, finite_goal]
   end