--- a/src/HOL/Tools/res_axioms.ML Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOL/Tools/res_axioms.ML Sun Feb 13 17:15:14 2005 +0100
@@ -292,8 +292,8 @@
end;
-fun sk_lookup [] t = None
- | sk_lookup ((tm,sk_tm)::tms) t = if (t = tm) then Some (sk_tm) else (sk_lookup tms t);
+fun sk_lookup [] t = NONE
+ | sk_lookup ((tm,sk_tm)::tms) t = if (t = tm) then SOME (sk_tm) else (sk_lookup tms t);
@@ -301,8 +301,8 @@
fun get_skolem epss t =
let val sk_fun = sk_lookup epss t
in
- case sk_fun of None => get_new_skolem epss t
- | Some sk => (sk,epss)
+ case sk_fun of NONE => get_new_skolem epss t
+ | SOME sk => (sk,epss)
end;