--- 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;