Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cterm_instantiate was calling a type instantiation function that works only for matching,
authorpaulson
Thu, 08 Feb 2007 18:14:13 +0100
changeset 22287 9985a79735c7
parent 22286 85b065601f45
child 22288 c565f33ec70f
cterm_instantiate was calling a type instantiation function that works only for matching, not unification as here.
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/drule.ML	Thu Feb 08 17:22:22 2007 +0100
+++ b/src/Pure/drule.ML	Thu Feb 08 18:14:13 2007 +0100
@@ -908,7 +908,7 @@
 fun cterm_instantiate ctpairs0 th =
   let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
       fun instT(ct,cu) =
-        let val inst = cterm_of thy o Envir.subst_TVars tye o term_of
+        let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of
         in (inst ct, inst cu) end
       fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
   in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
isabelle