| changeset 74282 | c2ee8d993d6a |
| parent 73020 | b51515722274 |
| child 77879 | dd222e2af01a |
--- a/src/HOL/Tools/numeral.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/numeral.ML Fri Sep 10 14:59:19 2021 +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 ([(v, T)], []); +fun instT T v = Thm.instantiate_cterm (TVars.make [(v, T)], Vars.empty); in