--- a/src/HOL/simpdata.ML Sat Jul 10 21:46:15 1999 +0200
+++ b/src/HOL/simpdata.ML Sat Jul 10 21:48:27 1999 +0200
@@ -31,7 +31,7 @@
else cla addSIs [th]
| _ => cla addSIs [th],
simp addsimps [th])
- handle _ => error ("AddIffs: theorem must be unconditional\n" ^
+ handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^
string_of_thm th);
fun delIff ((cla, simp), th) =
@@ -45,7 +45,7 @@
else cla delrules [th]
| _ => cla delrules [th],
simp delsimps [th])
- handle _ => (warning("DelIffs: ignoring conditional theorem\n" ^
+ handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^
string_of_thm th); (cla, simp));
fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)