src/Pure/thm.ML

--- a/src/Pure/thm.ML	Mon Mar 23 17:07:43 2015 +0100
+++ b/src/Pure/thm.ML	Mon Mar 23 19:43:03 2015 +0100
@@ -278,7 +278,7 @@
 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};
 
 
@@ -1306,8 +1306,8 @@
       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 =