src/HOL/Bali/Basis.thy

--- a/src/HOL/Bali/Basis.thy	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOL/Bali/Basis.thy	Sun Feb 13 17:15:14 2005 +0100
@@ -20,7 +20,7 @@
 
 ML {*
 fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat]
-  (fn _ => fn _ => fn t => if pred t then None else Some (mk_meta_eq thm));
+  (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm));
 *}
 
 declare split_if_asm  [split] option.split [split] option.split_asm [split]