diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/Tools/Compute_Oracle/linker.ML
--- 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