1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 25 12:52:21 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 25 13:39:34 2013 +0200
     1.3 @@ -579,17 +579,21 @@
     1.4  fun build_corec_args_direct_call lthy has_call sel_eqns sel =
     1.5    let
     1.6      val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
     1.7 -    fun rewrite_q t = if has_call t then @{term False} else @{term True};
     1.8 -    fun rewrite_g t = if has_call t then undef_const else t;
     1.9 -    fun rewrite_h t = if has_call t then HOLogic.mk_tuple (snd (strip_comb t)) else undef_const;
    1.10 -    fun massage _ NONE t = t
    1.11 -      | massage f (SOME {fun_args, rhs_term, ...}) t =
    1.12 -        massage_direct_corec_call lthy has_call f [] (range_type (fastype_of t)) rhs_term
    1.13 -        |> abs_tuple fun_args;
    1.14    in
    1.15 -    (massage rewrite_q maybe_sel_eqn,
    1.16 -     massage rewrite_g maybe_sel_eqn,
    1.17 -     massage rewrite_h maybe_sel_eqn)
    1.18 +    if is_none maybe_sel_eqn then (I, I, I) else
    1.19 +    let
    1.20 +      val {fun_args, rhs_term, ... } = the maybe_sel_eqn;
    1.21 +      fun rewrite_q t = if has_call t then @{term False} else @{term True};
    1.22 +      fun rewrite_g t = if has_call t then undef_const else t;
    1.23 +      fun rewrite_h t = if has_call t then HOLogic.mk_tuple (snd (strip_comb t)) else undef_const;
    1.24 +      fun massage f t =
    1.25 +          massage_direct_corec_call lthy has_call f [] (range_type (fastype_of t)) rhs_term
    1.26 +          |> abs_tuple fun_args;
    1.27 +    in
    1.28 +      (massage rewrite_q,
    1.29 +       massage rewrite_g,
    1.30 +       massage rewrite_h)
    1.31 +    end
    1.32    end;
    1.33  
    1.34  fun build_corec_arg_indirect_call lthy has_call sel_eqns sel =
    1.35 @@ -809,16 +813,10 @@
    1.36          fun prove_ctr disc_alist sel_alist disc_eqns sel_eqns {ctr, disc, sels, collapse, ...} =
    1.37            if not (exists (equal ctr o #ctr) disc_eqns)
    1.38                andalso not (exists (equal ctr o #ctr) sel_eqns)
    1.39 -(*
    1.40 -andalso (warning ("no eqns for ctr " ^ Syntax.string_of_term lthy ctr); true)
    1.41 -*)
    1.42              orelse (* don't try to prove theorems when some sel_eqns are missing *)
    1.43                filter (equal ctr o #ctr) sel_eqns
    1.44                |> fst o finds ((op =) o apsnd #sel) sels
    1.45                |> exists (null o snd)
    1.46 -(*
    1.47 -andalso (warning ("sel_eqn(s) missing for ctr " ^ Syntax.string_of_term lthy ctr); true)
    1.48 -*)
    1.49            then [] else
    1.50              let
    1.51                val (fun_name, fun_T, fun_args, prems) =
    1.52 @@ -842,7 +840,7 @@
    1.53                mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms
    1.54                |> K |> Goal.prove lthy [] [] t
    1.55                |> single
    1.56 -          end;
    1.57 +            end;
    1.58  
    1.59          val disc_alists = map3 (maps oo prove_disc) corec_specs exclssss disc_eqnss;
    1.60          val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss exclssss sel_eqnss;
    1.61 @@ -852,12 +850,13 @@
    1.62          val ctr_thmss = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss
    1.63            (map #ctr_specs corec_specs);
    1.64  
    1.65 -        val safess = map (map (K false)) ctr_thmss; (* FIXME: "true" for non-corecursive theorems *)
    1.66 +        val safess = map (map (not o exists_subterm (member (op =) (map SOME fun_names) o
    1.67 +          try (fst o dest_Free)) o snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o
    1.68 +          Logic.strip_imp_concl o drop_All o prop_of)) ctr_thmss;
    1.69          val safe_ctr_thmss = map (map snd o filter fst o (op ~~)) (safess ~~ ctr_thmss);
    1.70  
    1.71 -        fun mk_simp_thms disc_thms sel_thms ctr_thms = disc_thms @ sel_thms @ ctr_thms;
    1.72 -
    1.73 -        val simp_thmss = map3 mk_simp_thms disc_thmss sel_thmss safe_ctr_thmss;
    1.74 +        val simp_thmss =
    1.75 +          map3 (fn x => fn y => fn z => x @ y @ z) disc_thmss sel_thmss safe_ctr_thmss;
    1.76  
    1.77          val common_name = mk_common_name fun_names;
    1.78