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