841 Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn)) |
841 Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn)) |
842 else alt_name; |
842 else alt_name; |
843 |
843 |
844 val is_auxiliary = length cs >= 2; |
844 val is_auxiliary = length cs >= 2; |
845 val ((rec_const, (_, fp_def)), lthy') = lthy |
845 val ((rec_const, (_, fp_def)), lthy') = lthy |
846 |> is_auxiliary ? Local_Theory.concealed |
846 |> is_auxiliary ? Proof_Context.concealed |
847 |> Local_Theory.define |
847 |> Local_Theory.define |
848 ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), |
848 ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), |
849 ((Binding.concealed (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}), |
849 ((Binding.concealed (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}), |
850 fold_rev lambda params |
850 fold_rev lambda params |
851 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) |
851 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) |
852 ||> is_auxiliary ? Local_Theory.restore_naming lthy; |
852 ||> Proof_Context.restore_naming lthy; |
853 val fp_def' = |
853 val fp_def' = |
854 Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def]) |
854 Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def]) |
855 (Thm.cterm_of lthy' (list_comb (rec_const, params))); |
855 (Thm.cterm_of lthy' (list_comb (rec_const, params))); |
856 val specs = |
856 val specs = |
857 if length cs < 2 then [] |
857 if length cs < 2 then [] |