src/HOL/Tools/inductive.ML
changeset 32035 8e77b6a250d5
parent 31986 a68f88d264f7
child 32091 30e2ffbba718
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -922,7 +922,7 @@
     1.4          val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
     1.5            (Vartab.empty, Vartab.empty);
     1.6        in
     1.7 -        map (Envir.subst_vars tab) vars
     1.8 +        map (Envir.subst_term tab) vars
     1.9        end
    1.10    in
    1.11      map (mtch o apsnd prop_of) (cases ~~ intros)