462 (case AList.lookup op = params' u of |
462 (case AList.lookup op = params' u of |
463 SOME (_, (u', _)) => u' |
463 SOME (_, (u', _)) => u' |
464 | NONE => u)) |> |
464 | NONE => u)) |> |
465 Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |> |
465 Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |> |
466 eta_contract (member op = cs' orf is_pred pred_arities))) intros; |
466 eta_contract (member op = cs' orf is_pred pred_arities))) intros; |
467 val cnames_syn' = map (fn (b, _) => (Binding.map_name (suffix "p") b, NoSyn)) cnames_syn; |
467 val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn; |
468 val monos' = map (to_pred [] (Context.Proof ctxt)) monos; |
468 val monos' = map (to_pred [] (Context.Proof ctxt)) monos; |
469 val ({preds, intrs, elims, raw_induct, ...}, ctxt1) = |
469 val ({preds, intrs, elims, raw_induct, ...}, ctxt1) = |
470 InductivePackage.add_ind_def |
470 InductivePackage.add_ind_def |
471 {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty, |
471 {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty, |
472 coind = coind, no_elim = no_elim, no_ind = no_ind, |
472 coind = coind, no_elim = no_elim, no_ind = no_ind, |