author | Christian Urban <urbanc@in.tum.de> |
Tue, 19 Apr 2011 13:03:08 +0100 | |
changeset 2770 | fc21ba07e51e |
parent 2769 | 810e7303c70d |
child 2773 | d29a8a6f3138 |
--- a/Nominal/Nominal2.thy Mon Apr 18 15:57:45 2011 +0100 +++ b/Nominal/Nominal2.thy Tue Apr 19 13:03:08 2011 +0100 @@ -646,7 +646,7 @@ val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = tmp_thy - |> Sign.add_types pre_typs + |> Sign.add_types_global pre_typs |> prepare_dts dt_strs ||>> prepare_bn_funs bn_fun_strs bn_eq_strs ||>> prepare_bclauses dt_strs