--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Sun Oct 20 23:29:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Sun Oct 20 23:36:18 2013 +0200
@@ -1066,14 +1066,11 @@
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;
-val _ = tracing ("raw code theorem: " ^ Syntax.string_of_term lthy (prop_of raw_code_thm));
in
mk_primcorec_code_of_raw_code_tac lthy distincts 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;