diff -r 8408edac8f6b -r a6cad32a27b0 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Mar 27 14:41:07 2008 +0100
+++ b/src/Pure/tactic.ML	Thu Mar 27 14:41:09 2008 +0100
@@ -315,8 +315,9 @@
 (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
   increment revcut_rl instead.*)
 fun make_elim_preserve rl =
-  let val {maxidx,...} = rep_thm rl
-      fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT));
+  let val maxidx = Thm.maxidx_of rl
+      val thy = Thm.theory_of_thm rl
+      fun cvar ixn = cterm_of thy (Var(ixn,propT));
       val revcut_rl' =
           instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
                              (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl