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/HOL/Tools/Function/induction_schema.ML
changeset 74266 612b7e0d6721
parent 74200 17090e27aae9
child 77879 dd222e2af01a 
--- a/src/HOL/Tools/Function/induction_schema.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -381,7 +381,7 @@
 
     val res = Conjunction.intr_balanced (map_index project branches)
       |> fold_rev Thm.implies_intr (map Thm.cprop_of newgoals @ steps)
-      |> Drule.generalize (Symtab.empty, Symtab.make_set [Rn])
+      |> Drule.generalize (Names.empty, Names.make_set [Rn])
 
     val nbranches = length branches
     val npres = length pres
isabelle