src/HOL/Bali/Basis.thy
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Bali/Basis.thy	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  ML {*
     1.6  fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat]
     1.7 -  (fn _ => fn _ => fn t => if pred t then None else Some (mk_meta_eq thm));
     1.8 +  (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm));
     1.9  *}
    1.10  
    1.11  declare split_if_asm  [split] option.split [split] option.split_asm [split]