diff -r 54085e37ce4d -r 6676bf189852 src/ZF/Tools/inductive_package.ML
--- 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}));