src/Provers/Arith/assoc_fold.ML
changeset 15531 08c8dad8e399
parent 14387 e96d5c42c4b0
child 16423 24abe4c0e4b4
--- a/src/Provers/Arith/assoc_fold.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Provers/Arith/assoc_fold.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -57,8 +57,8 @@
        val th = Tactic.prove sg [] [] (Logic.mk_equals (lhs, rhs))
                    (fn _ => rtac Data.eq_reflection 1 THEN
                             simp_tac assoc_ss 1)
-   in Some th end
-   handle Assoc_fail => None;
+   in SOME th end
+   handle Assoc_fail => NONE;
 
 end;