# HG changeset patch
# User paulson
# Date 834748068 -7200
# Node ID d2f07baaf776a7b05acedbd295b821eeedac8ab2
# Parent  927a31ba43461c07e82e44f0488efea9587585ef
Now del_simp catches the right exception!

diff -r 927a31ba4346 -r d2f07baaf776 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jun 14 12:27:11 1996 +0200
+++ b/src/Pure/thm.ML	Fri Jun 14 12:27:48 1996 +0200
@@ -1441,7 +1441,7 @@
     None => mss
   | Some(rrule as {lhs,...}) =>
       Mss{net = (Net.delete_term((lhs,rrule),net,eq)
-                handle Net.INSERT =>
+                handle Net.DELETE =>
                  (prtm_warning "rewrite rule not in simpset" sign prop;
                   net)),
              congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}