825 val rec_name = |
825 val rec_name = |
826 if Binding.is_empty alt_name then |
826 if Binding.is_empty alt_name then |
827 Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn)) |
827 Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn)) |
828 else alt_name; |
828 else alt_name; |
829 |
829 |
|
830 val is_auxiliary = length cs >= 2; |
830 val ((rec_const, (_, fp_def)), lthy') = lthy |
831 val ((rec_const, (_, fp_def)), lthy') = lthy |
831 |> Local_Theory.conceal |
832 |> is_auxiliary ? Local_Theory.conceal |
832 |> Local_Theory.define |
833 |> Local_Theory.define |
833 ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), |
834 ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), |
834 ((Thm.def_binding rec_name, @{attributes [nitpick_unfold]}), |
835 ((Binding.conceal (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}), |
835 fold_rev lambda params |
836 fold_rev lambda params |
836 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) |
837 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) |
837 ||> Local_Theory.restore_naming lthy; |
838 ||> is_auxiliary ? Local_Theory.restore_naming lthy; |
838 val fp_def' = |
839 val fp_def' = |
839 Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def]) |
840 Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def]) |
840 (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params))); |
841 (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params))); |
841 val specs = |
842 val specs = |
842 if length cs < 2 then [] |
843 if length cs < 2 then [] |