diff -r 810e7303c70d -r fc21ba07e51e Nominal/Nominal2.thy
--- 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