equal
deleted
inserted
replaced
644 val thy = ProofContext.theory_of lthy |
644 val thy = ProofContext.theory_of lthy |
645 val tmp_thy = Theory.copy thy |
645 val tmp_thy = Theory.copy thy |
646 |
646 |
647 val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = |
647 val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = |
648 tmp_thy |
648 tmp_thy |
649 |> Sign.add_types pre_typs |
649 |> Sign.add_types_global pre_typs |
650 |> prepare_dts dt_strs |
650 |> prepare_dts dt_strs |
651 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
651 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
652 ||>> prepare_bclauses dt_strs |
652 ||>> prepare_bclauses dt_strs |
653 |
653 |
654 val bclauses' = complete dt_strs bclauses |
654 val bclauses' = complete dt_strs bclauses |