# HG changeset patch
# User blanchet
# Date 1388652622 -3600
# Node ID f4ae538b0ba5ea9accd23abeb8f834e61d4f405c
# Parent  f48ec7a80668642d88eba99ce6c4099f888e246e
gracefully handle single-equation case, where 'nchotomy' is 'True'

diff -r f48ec7a80668 -r f4ae538b0ba5 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- 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)