diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Matrix_LP/Compute_Oracle/linker.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -326,7 +326,7 @@
             let
                 val (newsubsts, instances) = Linker.add_instances thy instances monocs
                 val _ = if not (null newsubsts) then changed := true else ()
-                val newths = map (fn subst => Thm.instantiate (conv_subst thy subst, []) th) newsubsts
+                val newths = map (fn subst => Thm.instantiate (TVars.make (conv_subst thy subst), Vars.empty) th) newsubsts
 (*              val _ = if not (null newths) then (print ("added new theorems: ", newths); ()) else ()*)
                 val newmonos = fold (fn th => fn monos => (snd (collect_consts_of_thm th))@monos) newths []
             in