diff -r 6f43714517ee -r 08c8dad8e399 src/HOL/Modelcheck/EindhovenSyn.ML
--- a/src/HOL/Modelcheck/EindhovenSyn.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOL/Modelcheck/EindhovenSyn.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -26,7 +26,7 @@
 
 val pair_eta_expand_proc =
   Simplifier.simproc (Theory.sign_of (the_context ())) "pair_eta_expand" ["f::'a*'b=>'c"]
-  (fn _ => fn _ => fn t => case t of Abs _ => Some (mk_meta_eq pair_eta_expand) | _ => None);
+  (fn _ => fn _ => fn t => case t of Abs _ => SOME (mk_meta_eq pair_eta_expand) | _ => NONE);
 
 val Eindhoven_ss =
   simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];