equal
deleted
inserted
replaced
808 val (dts, lthy1) = prepare_dts dt_strs lthy0 |
808 val (dts, lthy1) = prepare_dts dt_strs lthy0 |
809 val ((bn_funs, bn_eqs), lthy2) = prepare_bn_funs bn_fun_strs bn_eq_strs lthy1 |
809 val ((bn_funs, bn_eqs), lthy2) = prepare_bn_funs bn_fun_strs bn_eq_strs lthy1 |
810 val bclauses = prepare_bclauses dt_strs lthy2 |
810 val bclauses = prepare_bclauses dt_strs lthy2 |
811 val bclauses' = complete dt_strs bclauses |
811 val bclauses' = complete dt_strs bclauses |
812 in |
812 in |
813 nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd |
813 timeit (fn () => nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd) |
814 end |
814 end |
815 |
815 |
816 |
816 |
817 (* Command Keyword *) |
817 (* Command Keyword *) |
818 |
818 |