diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 17 23:11:40 2009 +0200
@@ -342,7 +342,7 @@
                  val env = Pattern.first_order_match thy (ihypt, prop_of ihyp)
                    (Vartab.empty, Vartab.empty);
                  val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
-                   (map (Envir.subst_vars env) vs ~~
+                   (map (Envir.subst_term env) vs ~~
                     map (fold_rev (NominalDatatype.mk_perm [])
                       (rev pis' @ pis)) params' @ [z])) ihyp;
                  fun mk_pi th =