src/HOL/Tools/Datatype/datatype.ML

--- a/src/HOL/Tools/Datatype/datatype.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -649,7 +649,7 @@
     (* this theory is used just for parsing *)
     val tmp_thy = thy |>
       Theory.copy |>
-      Sign.add_types (map (fn (tvs, tname, mx, _) =>
+      Sign.add_types_global (map (fn (tvs, tname, mx, _) =>
         (tname, length tvs, mx)) dts);
 
     val (tyvars, _, _, _)::_ = dts;