equal
deleted
inserted
replaced
567 val constr_trms = flat (map mk_constr_trms dts') |
567 val constr_trms = flat (map mk_constr_trms dts') |
568 |
568 |
569 (* FIXME: local version *) |
569 (* FIXME: local version *) |
570 (* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *) |
570 (* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *) |
571 |
571 |
572 val thy' = Sign.add_consts_i constr_trms (Proof_Context.theory_of spec_ctxt) |
572 val thy' = Sign.add_consts constr_trms (Proof_Context.theory_of spec_ctxt) |
573 in |
573 in |
574 (dts', thy') |
574 (dts', thy') |
575 end |
575 end |
576 *} |
576 *} |
577 |
577 |
589 |
589 |
590 val bn_funs' = map prep_bn_fun bn_funs |
590 val bn_funs' = map prep_bn_fun bn_funs |
591 |
591 |
592 in |
592 in |
593 (Local_Theory.exit_global lthy') |
593 (Local_Theory.exit_global lthy') |
594 |> Sign.add_consts_i bn_funs' |
594 |> Sign.add_consts bn_funs' |
595 |> pair (bn_funs', bn_eqs) |
595 |> pair (bn_funs', bn_eqs) |
596 end |
596 end |
597 *} |
597 *} |
598 |
598 |
599 text {* associates every SOME with the index in the list; drops NONEs *} |
599 text {* associates every SOME with the index in the list; drops NONEs *} |