663 |
663 |
664 val ((rec_const, (_, fp_def)), lthy') = lthy |
664 val ((rec_const, (_, fp_def)), lthy') = lthy |
665 |> LocalTheory.conceal |
665 |> LocalTheory.conceal |
666 |> LocalTheory.define Thm.internalK |
666 |> LocalTheory.define Thm.internalK |
667 ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), |
667 ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), |
668 (Attrib.empty_binding, fold_rev lambda params |
668 ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]), |
|
669 fold_rev lambda params |
669 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) |
670 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) |
670 ||> LocalTheory.restore_naming lthy; |
671 ||> LocalTheory.restore_naming lthy; |
671 val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def]) |
672 val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def]) |
672 (cterm_of (ProofContext.theory_of lthy') (list_comb (rec_const, params))); |
673 (cterm_of (ProofContext.theory_of lthy') (list_comb (rec_const, params))); |
673 val specs = |
674 val specs = |