--- a/src/ZF/Tools/inductive_package.ML Thu Oct 28 20:32:40 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Oct 28 20:38:21 2021 +0200
@@ -506,7 +506,7 @@
val inst =
case elem_frees of [_] => I
| _ => Drule.instantiate_normalize (TVars.empty,
- Vars.make [(\<^var>\<open>?x1::i\<close>, Thm.global_cterm_of thy4 elem_tuple)]);
+ Vars.make [((("x", 1), \<^Type>\<open>i\<close>), Thm.global_cterm_of thy4 elem_tuple)]);
(*strip quantifier and the implication*)
val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp}));