src/HOL/Nominal/nominal_inductive2.ML
changeset 32035 8e77b6a250d5
parent 31938 f193d95b4632
child 32134 ee143615019c
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4    let val env = Pattern.first_order_match thy (p, prop_of th)
     1.5      (Vartab.empty, Vartab.empty)
     1.6    in Thm.instantiate ([],
     1.7 -    map (Envir.subst_vars env #> cterm_of thy) vs ~~ cts) th
     1.8 +    map (Envir.subst_term env #> cterm_of thy) vs ~~ cts) th
     1.9    end;
    1.10  
    1.11  fun prove_strong_ind s avoids ctxt =