--- a/src/HOL/MiniML/Maybe.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Maybe.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -18,7 +18,7 @@
 (* expansion of option_bind *)
 Goalw [option_bind_def] "P(option_bind res f) = \
 \         ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
-by (rtac split_option_case 1);
+by (rtac option.split 1);
 qed "split_option_bind";
 
 Goal