equal
deleted
inserted
replaced
847 fold_rev lambda params |
847 fold_rev lambda params |
848 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) |
848 (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) |
849 ||> is_auxiliary ? Local_Theory.restore_naming lthy; |
849 ||> is_auxiliary ? Local_Theory.restore_naming lthy; |
850 val fp_def' = |
850 val fp_def' = |
851 Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def]) |
851 Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def]) |
852 (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params))); |
852 (Proof_Context.cterm_of lthy' (list_comb (rec_const, params))); |
853 val specs = |
853 val specs = |
854 if length cs < 2 then [] |
854 if length cs < 2 then [] |
855 else |
855 else |
856 map_index (fn (i, (name_mx, c)) => |
856 map_index (fn (i, (name_mx, c)) => |
857 let |
857 let |