--- 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];