# HG changeset patch
# User berghofe
# Date 1079528445 -3600
# Node ID 5688b05b2575bc2bf630fc932329c08ea3aed455
# Parent  1ffe42cfaefe3eb9ed416c1ae18cb0d821c91b65
case_tac no longer raises THM exception if goal number is out of range.

diff -r 1ffe42cfaefe -r 5688b05b2575 src/HOL/Tools/datatype_package.ML
--- 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);