--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Mon Mar 23 17:07:43 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Mon Mar 23 19:43:03 2015 +0100
@@ -62,7 +62,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 =