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/Tools/Compute_Oracle/linker.ML
changeset 32035 8e77b6a250d5
parent 31971 8c1b845ed105
child 32740 9dd0a2f83429 
--- a/src/Tools/Compute_Oracle/linker.ML	Fri Jul 17 22:54:11 2009 +0200
+++ b/src/Tools/Compute_Oracle/linker.ML	Fri Jul 17 23:11:40 2009 +0200
@@ -341,7 +341,7 @@
 	    let
 		val (newsubsts, instances) = Linker.add_instances thy instances monocs
 		val _ = if not (null newsubsts) then changed := true else ()
-		val newpats = map (fn subst => Envir.subst_TVars subst p) newsubsts
+		val newpats = map (fn subst => Envir.subst_term_types subst p) newsubsts
 	    in
 		PolyPattern (p, instances, instancepats@newpats)
 	    end
isabelle