# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1303214588 -3600
# Node ID fc21ba07e51e665a4828a32597cdfa20929d881f
# Parent  810e7303c70defe494672fec1e3d882e69491bfc
updated to snapshot Isabelle 19 April

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