updated to snapshot Isabelle 19 April
authorChristian Urban <urbanc@in.tum.de>
Tue, 19 Apr 2011 13:03:08 +0100
changeset 2770 fc21ba07e51e
parent 2769 810e7303c70d
child 2773 d29a8a6f3138
updated to snapshot Isabelle 19 April
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