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/HOL/Tools/Meson/meson.ML
changeset 74282 c2ee8d993d6a
parent 74075 a5bab59d580b
child 74346 55007a70bd96 
--- a/src/HOL/Tools/Meson/meson.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -358,7 +358,8 @@
       val ([x], ctxt') =
         Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
       val spec' = spec
-        |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]);
+        |> Thm.instantiate
+          (TVars.empty, Vars.make [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]);
     in (th RS spec', ctxt') end
 end;
isabelle