case_tac no longer raises THM exception if goal number is out of range.

--- a/src/HOL/Tools/datatype_package.ML	Mon Mar 15 10:58:49 2004 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Mar 17 14:00:45 2004 +0100
@@ -233,7 +233,7 @@
         else case_inst_tac inst_tac t
                (#exhaustion (datatype_info_sg_err (Thm.sign_of_thm state) tn))
                i state
-      end;
+      end handle THM _ => Seq.empty;
 
 fun case_tac t = gen_case_tac Tactic.res_inst_tac (t, None);