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/ZF/Tools/inductive_package.ML
changeset 74282 c2ee8d993d6a
parent 71080 64249a83bc29
child 74290 b2ad24b5a42c 
--- a/src/ZF/Tools/inductive_package.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -508,7 +508,7 @@
        The name "x.1" comes from the "RS spec" !*)
      val inst =
          case elem_frees of [_] => I
-            | _ => Drule.instantiate_normalize ([], [(((("x",1), Ind_Syntax.iT)),
+            | _ => Drule.instantiate_normalize (TVars.empty, Vars.make [(((("x",1), Ind_Syntax.iT)),
                                       Thm.global_cterm_of thy4 elem_tuple)]);
 
      (*strip quantifier and the implication*)
isabelle