| changeset 77879 | dd222e2af01a |
| parent 74282 | c2ee8d993d6a |
| child 82380 | ceb4f33d3073 |
--- a/src/HOL/Tools/numeral.ML Tue Apr 18 21:47:40 2023 +0200 +++ b/src/HOL/Tools/numeral.ML Tue Apr 18 22:24:48 2023 +0200 @@ -64,7 +64,7 @@ val uminus_tvar = tvar \<^sort>\<open>uminus\<close>; val uminus = cterm_of (Const (\<^const_name>\<open>uminus\<close>, TVar uminus_tvar --> TVar uminus_tvar)); -fun instT T v = Thm.instantiate_cterm (TVars.make [(v, T)], Vars.empty); +fun instT T v = Thm.instantiate_cterm (TVars.make1 (v, T), Vars.empty); in