# HG changeset patch
# User wenzelm
# Date 924860917 -7200
# Node ID 937eb94b2aab8499e370ce92d623e8a13d964797
# Parent  7954ffeb93f3c1e3fe94d9cabf5229c444eb9297
oops;

diff -r 7954ffeb93f3 -r 937eb94b2aab src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Apr 22 18:25:24 1999 +0200
+++ b/src/Provers/classical.ML	Fri Apr 23 11:48:37 1999 +0200
@@ -934,7 +934,7 @@
       let
         fun may_unify net = Net.unify_term net o #prop o Thm.rep_thm;
         fun erules_of (_, enet) = order_rules (flat (map (may_unify enet) facts));
-      in flat (map erules_of nets) end;
+      in flat (map erules_of nets) @ [Data.not_elim, imp_elim] end;
 
 
 (* trace rules *)
@@ -954,7 +954,7 @@
   let
     val CS {safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...} = cs;
     val nets = [safe0_netpair, safep_netpair, haz_netpair, dup_netpair];
-    val erules = Data.not_elim :: imp_elim :: find_erules facts nets;
+    val erules = find_erules facts nets;
 
     val tac = SUBGOAL (fn (goal, i) =>
       let