--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Sun Dec 10 12:54:52 2023 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Sun Dec 10 13:39:40 2023 +0100
@@ -61,7 +61,7 @@
let
val ctxt = Proof_Context.init_global thy
val maxidx = fold (Term.maxidx_term o Thm.prop_of) intros ~1
- val pats = map (Logic.incr_indexes ([], [], maxidx + 1)) pats
+ val pats = map (Logic.incr_indexes ([], maxidx + 1)) pats
val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
val result_pats = map Var (fold_rev Term.add_vars pats [])
fun mk_fresh_name names =