1.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Sat May 15 18:29:18 2010 +0200
     1.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Sat May 15 21:09:54 2010 +0200
     1.3 @@ -159,8 +159,6 @@
     1.4    in mtch env (t,ct) end;
     1.5  
     1.6  
     1.7 -fun mp prem rule = implies_elim rule prem;
     1.8 -
     1.9  fun discharge prems rule =
    1.10    let
    1.11       val thy = theory_of_thm (hd prems);
    1.12 @@ -172,7 +170,7 @@
    1.13       val insts' = map (fn (idxn,ct) => (cterm_of thy (Var (idxn,typ_of (ctyp_of_term ct))),ct))  
    1.14                       insts;
    1.15       val rule' = Thm.instantiate (tyinsts',insts') rule;
    1.16 -   in fold mp prems rule' end;
    1.17 +   in fold Thm.elim_implies prems rule' end;
    1.18  
    1.19  local
    1.20