src/Tools/induct.ML
changeset 44241 7943b69f0188
parent 43333 2bdec7f430d3
child 44942 a05ab4d803f2
     1.1 --- a/src/Tools/induct.ML	Wed Aug 17 16:46:58 2011 +0200
     1.2 +++ b/src/Tools/induct.ML	Wed Aug 17 18:05:31 2011 +0200
     1.3 @@ -658,7 +658,7 @@
     1.4      fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
     1.5        | goal_concl 0 xs B =
     1.6            if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
     1.7 -          else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B))
     1.8 +          else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B))
     1.9        | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
    1.10        | goal_concl _ _ _ = NONE;
    1.11    in