# HG changeset patch
# User blanchet
# Date 1389366661 -3600
# Node ID afc156c7e4f7bf100f0d722a9e540cfc87019c5e
# Parent  63a5e0d8ce3bdd071dd8e6b9891e0991296033db
cope gracefully with missing ctr equations by plugging in 'False ==> ...'

diff -r 63a5e0d8ce3b -r afc156c7e4f7 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 15:48:13 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 16:11:01 2014 +0100
@@ -1172,7 +1172,8 @@
                       val raw_rhs = expand_corec_code_rhs lthy has_call bound_Ts rhs;
                       val cond_ctrs =
                         fold_rev_corec_code_rhs lthy (K oo (cons oo pair)) bound_Ts raw_rhs [];
-                      val ctr_thms = map (the o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
+                      val ctr_thms =
+                        map (the_default FalseE o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
                     in SOME (false, rhs, raw_rhs, ctr_thms) end
                   | NONE =>
                     let
@@ -1221,13 +1222,13 @@
                     val (distincts, discIs, sel_splits, sel_split_asms) =
                       case_thms_of_term lthy bound_Ts raw_rhs;
 
-                    val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs
-                        sel_splits sel_split_asms ms ctr_thms
+                    val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs sel_splits
+                        sel_split_asms ms ctr_thms
                         (if exhaustive_code then try the_single nchotomys else NONE)
                       |> K |> Goal.prove_sorry lthy [] [] raw_goal
                       |> Thm.close_derivation;
                   in
-                    mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
+                    mk_primcorec_code_tac lthy distincts sel_splits raw_code_thm
                     |> K |> Goal.prove_sorry lthy [] [] goal
                     |> Thm.close_derivation
                     |> single
diff -r 63a5e0d8ce3b -r afc156c7e4f7 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 10 15:48:13 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 10 16:11:01 2014 +0100
@@ -8,7 +8,7 @@
 signature BNF_GFP_REC_SUGAR_TACTICS =
 sig
   val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
-  val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
+  val mk_primcorec_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
   val mk_primcorec_ctr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
@@ -16,8 +16,8 @@
     thm list -> tactic
   val mk_primcorec_exhaust_tac: Proof.context -> string list -> int -> thm -> tactic
   val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic
-  val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
-    thm list -> int list -> thm list -> thm option -> tactic
+  val mk_primcorec_raw_code_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
+    int list -> thm list -> thm option -> tactic
   val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
     thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
 end;
@@ -157,7 +157,7 @@
     end
   | _ => split);
 
-fun raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
+fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
   let
     val splits' =
       map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits)
@@ -177,8 +177,7 @@
 
 fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
 
-fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms fun_ctrs
-    nchotomy_opt =
+fun mk_primcorec_raw_code_tac ctxt distincts discIs splits split_asms ms fun_ctrs nchotomy_opt =
   let
     val n = length ms;
     val (ms', fun_ctrs') =
@@ -192,13 +191,12 @@
          ||> (fn thm => [rulify_nchotomy n nchotomy RS thm] handle THM _ => [thm])
          |> op @));
   in
-    EVERY (map2 (raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
-      ms' fun_ctrs') THEN
+    EVERY (map2 (raw_code_single_tac ctxt distincts discIs splits split_asms) ms' fun_ctrs') THEN
     IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
       HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)))
   end;
 
-fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw =
+fun mk_primcorec_code_tac ctxt distincts splits raw =
   HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'
     SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
     (rtac refl ORELSE' atac ORELSE'