src/Pure/Isar/rule_insts.ML

--- a/src/Pure/Isar/rule_insts.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -312,7 +312,7 @@
               (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
               (xis ~~ ts));
         (* Lift and instantiate rule *)
-        val {maxidx, ...} = rep_thm st;
+        val maxidx = Thm.maxidx_of st;
         val paramTs = map #2 params
         and inc = maxidx+1
         fun liftvar (Var ((a,j), T)) =