--- a/src/FOL/eqrule_FOL_data.ML Fri Feb 11 18:51:00 2005 +0100
+++ b/src/FOL/eqrule_FOL_data.ML Sun Feb 13 17:15:14 2005 +0100
@@ -17,10 +17,10 @@
struct
fun mk_eq th = case concl_of th of
- Const("==",_)$_$_ => Some (th)
- | _$(Const("op <->",_)$_$_) => Some (th RS iff_reflection)
- | _$(Const("op =",_)$_$_) => Some (th RS eq_reflection)
- | _ => None;
+ Const("==",_)$_$_ => SOME (th)
+ | _$(Const("op <->",_)$_$_) => SOME (th RS iff_reflection)
+ | _$(Const("op =",_)$_$_) => SOME (th RS eq_reflection)
+ | _ => NONE;
val tranformation_pairs =
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
@@ -37,8 +37,8 @@
(case Term.head_of p of
Const(a,_) =>
(case Library.assoc(pairs,a) of
- Some(rls) => flat (map atoms ([th] RL rls))
- | None => [th])
+ SOME(rls) => flat (map atoms ([th] RL rls))
+ | NONE => [th])
| _ => [th])
| _ => [th])
in atoms end;