equal
deleted
inserted
replaced
506 |
506 |
507 val ((R, RIntro_thmss, R_elim), lthy) = |
507 val ((R, RIntro_thmss, R_elim), lthy) = |
508 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy |
508 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy |
509 |
509 |
510 val lthy = PROFILE "abbrev" |
510 val lthy = PROFILE "abbrev" |
511 (LocalTheory.abbrevs ("", false) (* FIXME really this mode? cf. Syntax.default_mode *) |
511 (TermSyntax.abbrevs Syntax.default_mode [((defname ^ "_dom", NoSyn), mk_acc domT R)]) lthy |
512 [((defname ^ "_dom", NoSyn), mk_acc domT R)]) lthy |
|
513 |
512 |
514 val newthy = ProofContext.theory_of lthy |
513 val newthy = ProofContext.theory_of lthy |
515 val clauses = map (transfer_clause_ctx newthy) clauses |
514 val clauses = map (transfer_clause_ctx newthy) clauses |
516 |
515 |
517 val cert = cterm_of (ProofContext.theory_of lthy) |
516 val cert = cterm_of (ProofContext.theory_of lthy) |