author | blanchet |
Thu, 02 Jan 2014 09:50:22 +0100 | |
changeset 54908 | f4ae538b0ba5 |
parent 54907 | f48ec7a80668 |
child 54909 | 63db983c6953 |
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 09:50:22 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 09:50:22 2014 +0100 @@ -160,7 +160,7 @@ fun_ctrs |> split_last ||> unfold_thms ctxt [atomize_conjL] - ||> (fn thm => [rulify_nchotomy n nchotomy RS thm]) + ||> (fn thm => [rulify_nchotomy n nchotomy RS thm] handle THM _ => [thm]) |> op @)); in EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)