changeset 2770 | fc21ba07e51e |
parent 2768 | 639979b7fa6e |
child 2781 | 542ff50555f5 |
--- 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