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/split_rule.ML
changeset 77879 dd222e2af01a
parent 74282 c2ee8d993d6a 
--- a/src/HOL/Tools/split_rule.ML	Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/split_rule.ML	Tue Apr 18 22:24:48 2023 +0200
@@ -42,7 +42,7 @@
 fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl =
       let val T' = HOLogic.flatten_tupleT T1 ---> T2;
           val newt = ap_split T1 T2 (Var (v, T'));
-      in Thm.instantiate (TVars.empty, Vars.make [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end
+      in Thm.instantiate (TVars.empty, Vars.make1 (dest_Var t, Thm.cterm_of ctxt newt)) rl end
   | split_rule_var' _ _ rl = rl;
isabelle