diff -r 4b1a63678839 -r 7943b69f0188 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/Tools/induct.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -658,7 +658,7 @@
     fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
       | goal_concl 0 xs B =
           if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
-          else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B))
+          else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B))
       | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
       | goal_concl _ _ _ = NONE;
   in