Now del_simp catches the right exception!
authorpaulson
Fri, 14 Jun 1996 12:27:48 +0200
changeset 1802 d2f07baaf776
parent 1801 927a31ba4346
child 1803 ff4cb897dfd3
Now del_simp catches the right exception!
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}