case_tac no longer raises THM exception if goal number is out of range.
authorberghofe
Wed Mar 17 14:00:45 2004 +0100 (2004-03-17)
changeset 144715688b05b2575
parent 14470 1ffe42cfaefe
child 14472 cba7c0a3ffb3
case_tac no longer raises THM exception if goal number is out of range.
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Mar 15 10:58:49 2004 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Mar 17 14:00:45 2004 +0100
     1.3 @@ -233,7 +233,7 @@
     1.4          else case_inst_tac inst_tac t
     1.5                 (#exhaustion (datatype_info_sg_err (Thm.sign_of_thm state) tn))
     1.6                 i state
     1.7 -      end;
     1.8 +      end handle THM _ => Seq.empty;
     1.9  
    1.10  fun case_tac t = gen_case_tac Tactic.res_inst_tac (t, None);
    1.11