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 77879 dd222e2af01a
parent 74501 0803dd7f920d
child 80306 c2537860ccf8 
--- a/src/HOL/Tools/Meson/meson.ML	Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Tue Apr 18 22:24:48 2023 +0200
@@ -358,7 +358,7 @@
         Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
       val spec' = spec
         |> Thm.instantiate
-          (TVars.empty, Vars.make [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]);
+          (TVars.empty, Vars.make1 (spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var))));
     in (th RS spec', ctxt') end
 end;
isabelle