Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nominal/nominal_inductive.ML
changeset 32035 8e77b6a250d5
parent 31938 f193d95b4632
child 32149 ef59550a55d3 
--- 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 =
isabelle