src/Pure/thm.ML

     Cterm {maxidx = Int.max (maxidx_of_term t, i), thy = thy, t = t, T = T, sorts = sorts};
 
 fun incr_indexes_cterm i (ct as Cterm {thy, t, T, maxidx, sorts}) =
   if i < 0 then raise CTERM ("negative increment", [ct])
   else if i = 0 then ct
-  else Cterm {thy = thy, t = Logic.incr_indexes ([], i) t,
+  else Cterm {thy = thy, t = Logic.incr_indexes ([], [], i) t,
     T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};
 
 
 (* matching *)
 

      {thy = thy,
       tags = [],
       maxidx = maxidx + i,
       shyps = shyps,
       hyps = hyps,
-      tpairs = map (apply2 (Logic.incr_indexes ([], i))) tpairs,
-      prop = Logic.incr_indexes ([], i) prop});
+      tpairs = map (apply2 (Logic.incr_indexes ([], [], i))) tpairs,
+      prop = Logic.incr_indexes ([], [], i) prop});
 
 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
 fun assumption opt_ctxt i state =
   let
     val Thm (der, {thy, maxidx, shyps, hyps, ...}) = state;