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;