src/Pure/tactic.ML
changeset 26424 a6cad32a27b0
parent 25939 ddea202704b4
child 26626 c6231d64d264
     1.1 --- a/src/Pure/tactic.ML	Thu Mar 27 14:41:07 2008 +0100
     1.2 +++ b/src/Pure/tactic.ML	Thu Mar 27 14:41:09 2008 +0100
     1.3 @@ -315,8 +315,9 @@
     1.4  (*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
     1.5    increment revcut_rl instead.*)
     1.6  fun make_elim_preserve rl =
     1.7 -  let val {maxidx,...} = rep_thm rl
     1.8 -      fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT));
     1.9 +  let val maxidx = Thm.maxidx_of rl
    1.10 +      val thy = Thm.theory_of_thm rl
    1.11 +      fun cvar ixn = cterm_of thy (Var(ixn,propT));
    1.12        val revcut_rl' =
    1.13            instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
    1.14                               (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl