--- a/src/HOL/Statespace/distinct_tree_prover.ML Sat May 15 18:29:18 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Sat May 15 21:09:54 2010 +0200
@@ -159,8 +159,6 @@
in mtch env (t,ct) end;
-fun mp prem rule = implies_elim rule prem;
-
fun discharge prems rule =
let
val thy = theory_of_thm (hd prems);
@@ -172,7 +170,7 @@
val insts' = map (fn (idxn,ct) => (cterm_of thy (Var (idxn,typ_of (ctyp_of_term ct))),ct))
insts;
val rule' = Thm.instantiate (tyinsts',insts') rule;
- in fold mp prems rule' end;
+ in fold Thm.elim_implies prems rule' end;
local