--- a/src/Provers/Arith/abel_cancel.ML Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Provers/Arith/abel_cancel.ML Sun Feb 13 17:15:14 2005 +0100
@@ -119,8 +119,8 @@
simp_tac prepare_ss 1 THEN
IF_UNSOLVED (simp_tac cancel_ss 1) THEN
IF_UNSOLVED (simp_tac inverse_ss 1))
- in Some thm end
- handle Cancel => None;
+ in SOME thm end
+ handle Cancel => NONE;
val sum_conv =
@@ -178,8 +178,8 @@
simp_tac prepare_ss 1 THEN
simp_tac sum_cancel_ss 1 THEN
IF_UNSOLVED (simp_tac add_ac_ss 1))
- in Some thm end
- handle Cancel => None;
+ in SOME thm end
+ handle Cancel => NONE;
val rel_conv =
Simplifier.simproc_i (Sign.deref sg_ref) "cancel_relations"