1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Tue Sep 24 21:27:45 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Tue Sep 24 22:21:51 2013 +0200
     1.3 @@ -526,9 +526,11 @@
     1.4      val sel_imp_rhss = (sels ~~ ctr_args)
     1.5        |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg));
     1.6  
     1.7 +(*
     1.8  val _ = tracing ("reduced\n    " ^ Syntax.string_of_term @{context} imp_rhs ^ "\nto\n    \<cdot> " ^
     1.9   (is_some maybe_eqn_data_disc ? K (Syntax.string_of_term @{context} disc_imp_rhs ^ "\n    \<cdot> ")) "" ^
    1.10   space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) sel_imp_rhss));
    1.11 +*)
    1.12  
    1.13      val eqns_data_sel =
    1.14        map (co_dissect_eqn_sel fun_names corec_specs eqn' (SOME ctr)) sel_imp_rhss;
    1.15 @@ -652,8 +654,10 @@
    1.16        | currys Ts t = t $ mk_tuple1 (List.rev Ts) (map Bound (length Ts - 1 downto 0))
    1.17            |> fold_rev (Term.abs o pair Name.uu) Ts;
    1.18  
    1.19 +(*
    1.20  val _ = tracing ("corecursor arguments:\n    \<cdot> " ^
    1.21   space_implode "\n    \<cdot> " (map (Syntax.string_of_term lthy) corec_args));
    1.22 +*)
    1.23  
    1.24      val exclss' =
    1.25        disc_eqnss
    1.26 @@ -739,8 +743,10 @@
    1.27        else if simple then SOME (K (auto_tac lthy))
    1.28        else NONE;
    1.29  
    1.30 +(*
    1.31  val _ = tracing ("exclusiveness properties:\n    \<cdot> " ^
    1.32   space_implode "\n    \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) exclss'));
    1.33 +*)
    1.34  
    1.35      val exclss'' = exclss' |> map (map (fn (idx, t) =>
    1.36        (idx, (Option.map (Goal.prove lthy [] [] t) (prove_excl_tac idx), t))));
    1.37 @@ -808,12 +814,16 @@
    1.38          fun prove_ctr disc_alist sel_alist disc_eqns sel_eqns {ctr, disc, sels, collapse, ...} =
    1.39            if not (exists (equal ctr o #ctr) disc_eqns)
    1.40                andalso not (exists (equal ctr o #ctr) sel_eqns)
    1.41 +(*
    1.42  andalso (warning ("no eqns for ctr " ^ Syntax.string_of_term lthy ctr); true)
    1.43 +*)
    1.44              orelse (* don't try to prove theorems when some sel_eqns are missing *)
    1.45                filter (equal ctr o #ctr) sel_eqns
    1.46                |> fst o finds ((op =) o apsnd #sel) sels
    1.47                |> exists (null o snd)
    1.48 +(*
    1.49  andalso (warning ("sel_eqn(s) missing for ctr " ^ Syntax.string_of_term lthy ctr); true)
    1.50 +*)
    1.51            then [] else
    1.52              let
    1.53                val (fun_name, fun_T, fun_args, prems) =