removed temporary error handling
authorblanchet
Sun, 20 Oct 2013 23:36:18 +0200
changeset 54175 83145b857bb9
parent 54174 c6291ae7cd18
child 54176 8039bd7e98b1
removed temporary error handling
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- 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;