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 81519 cdc43c0fdbfc
parent 79971 033f90dc441d 
--- a/src/HOL/Tools/Function/induction_schema.ML	Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Nov 30 22:33:21 2024 +0100
@@ -121,7 +121,8 @@
     val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
 
     val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
-    val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
+    val (Pbool :: xs') =
+      map Free (Variable.variant_names (fold Variable.declare_names allqnames ctxt) (("P", HOLogic.boolT) :: xs))
     val Cs' = map (Pattern.rewrite_term (Proof_Context.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
 
     fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
isabelle