736 val _ = null cnames_syn andalso error "No inductive predicates given"; |
736 val _ = null cnames_syn andalso error "No inductive predicates given"; |
737 val names = map (Binding.base_name o fst) cnames_syn; |
737 val names = map (Binding.base_name o fst) cnames_syn; |
738 val _ = message (quiet_mode andalso not verbose) |
738 val _ = message (quiet_mode andalso not verbose) |
739 ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names); |
739 ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names); |
740 |
740 |
741 val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn; (* FIXME *) |
741 val cnames = map (LocalTheory.full_name ctxt o #1) cnames_syn; (* FIXME *) |
742 val ((intr_names, intr_atts), intr_ts) = |
742 val ((intr_names, intr_atts), intr_ts) = |
743 apfst split_list (split_list (map (check_rule ctxt cs params) intros)); |
743 apfst split_list (split_list (map (check_rule ctxt cs params) intros)); |
744 |
744 |
745 val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds, |
745 val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds, |
746 argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts |
746 argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts |