--- a/src/Tools/eqsubst.ML Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Tools/eqsubst.ML Sat Jul 27 16:35:51 2013 +0200
@@ -252,7 +252,7 @@
RW_Inst.rw ctxt m rule conclthm
|> unfix_frees cfvs
|> Conv.fconv_rule Drule.beta_eta_conversion
- |> (fn r => Tactic.rtac r i st);
+ |> (fn r => rtac r i st);
(* substitute within the conclusion of goal i of gth, using a meta
equation rule. Note that we assume rule has var indicies zero'd *)
@@ -334,8 +334,7 @@
|> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
in
(* ~j because new asm starts at back, thus we subtract 1 *)
- Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))
- (Tactic.dtac preelimrule i st2)
+ Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dtac preelimrule i st2)
end;