src/HOL/Tools/res_axioms.ML

     in
 	(sk_term,(t,sk_term)::epss)
     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);
 
 
 
 (* get the proper skolem term to replace epsilon term *)
 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;
 
 
 fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = get_skolem epss t
   | rm_Eps_cls_aux epss (P $ Q) =