src/Pure/type.ML

--- a/src/Pure/type.ML	Tue Mar 31 20:18:10 2015 +0200
+++ b/src/Pure/type.ML	Tue Mar 31 21:12:22 2015 +0200
@@ -659,8 +659,9 @@
   let
     val types' = f types;
     val _ =
+      not (Name_Space.defined types' "dummy") orelse
       Name_Space.intern (Name_Space.space_of_table types') "dummy" = "dummy" orelse
-        error "Illegal declaration of dummy type";
+      error "Illegal declaration of dummy type";
   in (classes, default, types') end);
 
 fun syntactic tsig (Type (c, Ts)) =