# HG changeset patch
# User blanchet
# Date 1381740949 -7200
# Node ID e5f853482006d7677c02654144cd925b2411938f
# Parent  865b05fcc8b8daa4df8bd6565afe46a68ea3f74b
keep temporary error handling in there until code equations are properly generated

diff -r 865b05fcc8b8 -r e5f853482006 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 14 10:50:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 14 10:55:49 2013 +0200
@@ -1015,12 +1015,15 @@
                 val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs sel_splits
                     sel_split_asms ms ctr_thms
                   |> K |> Goal.prove lthy [] [] raw_t;
-              in
-                mk_primcorec_code_of_raw_code_tac lthy sel_splits raw_code_thm
-                |> K |> Goal.prove lthy [] [] t
-                |> single
-              end
-          end;
+val _ = tracing ("raw code theorem: " ^ Syntax.string_of_term lthy (prop_of raw_code_thm));
+               in
+                 mk_primcorec_code_of_raw_code_tac lthy sel_splits raw_code_thm
+                 |> K |> Goal.prove lthy [] [] t
+|> tap (tracing o curry (op ^) "code theorem: " o Syntax.string_of_term lthy o prop_of)
+                 |> single
+               end
+handle ERROR s => (warning s; []) (*###*)
+           end;
 
         val disc_alists = map3 (maps oo prove_disc) corec_specs exclssss disc_eqnss;
         val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss exclssss sel_eqnss;