diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Option.ML
--- a/src/HOL/Option.ML	Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Option.ML	Fri Jul 24 13:03:20 1998 +0200
@@ -8,7 +8,7 @@
 open Option;
 
 qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
-	(K [option.induct_tac "x" 1, Auto_tac]);
+	(K [induct_tac "x" 1, Auto_tac]);
 
 section "case analysis in premises";
 
@@ -55,7 +55,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]);
+ (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]);
 AddIffs[option_map_eq_Some];
 
 section "o2s";