equal
deleted
inserted
replaced
438 fun gen_add_split bang split ctxt = |
438 fun gen_add_split bang split ctxt = |
439 let |
439 let |
440 val (name, asm) = split_thm_info split |
440 val (name, asm) = split_thm_info split |
441 val split0 = Thm.trim_context split |
441 val split0 = Thm.trim_context split |
442 fun tac ctxt' = |
442 fun tac ctxt' = |
443 let val split' = Thm.transfer (Proof_Context.theory_of ctxt') split0 in |
443 let val split' = Thm.transfer' ctxt' split0 in |
444 (if asm then split_asm_tac ctxt' [split'] |
444 (if asm then split_asm_tac ctxt' [split'] |
445 else if bang |
445 else if bang |
446 then split_tac ctxt' [split'] THEN_ALL_NEW |
446 then split_tac ctxt' [split'] THEN_ALL_NEW |
447 TRY o (SELECT_GOAL (Data.safe_tac ctxt')) |
447 TRY o (SELECT_GOAL (Data.safe_tac ctxt')) |
448 else split_tac ctxt' [split']) |
448 else split_tac ctxt' [split']) |