src/HOL/Option.ML

--- a/src/HOL/Option.ML	Mon Apr 27 18:06:22 1998 +0200
+++ b/src/HOL/Option.ML	Mon Apr 27 19:29:19 1998 +0200
@@ -56,8 +56,7 @@
 val option_map_eq_Some = prove_goalw thy [option_map_def]
 	"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" 
  (K [asm_full_simp_tac (simpset() addsplits [split_option_case]) 1]);
-AddSDs[option_map_eq_Some RS iffD1];
-Addsimps [option_map_eq_Some];
+AddIffs[option_map_eq_Some];
 
 section "o2s";