--- 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