src/HOL/Nominal/nominal_inductive.ML
changeset 32035 8e77b6a250d5
parent 31938 f193d95b4632
child 32149 ef59550a55d3
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -342,7 +342,7 @@
     1.4                   val env = Pattern.first_order_match thy (ihypt, prop_of ihyp)
     1.5                     (Vartab.empty, Vartab.empty);
     1.6                   val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
     1.7 -                   (map (Envir.subst_vars env) vs ~~
     1.8 +                   (map (Envir.subst_term env) vs ~~
     1.9                      map (fold_rev (NominalDatatype.mk_perm [])
    1.10                        (rev pis' @ pis)) params' @ [z])) ihyp;
    1.11                   fun mk_pi th =