src/Pure/type.ML
changeset 21858 05f57309170c
parent 21116 be58cded79da
child 21934 ba683b0b2456
     1.1 --- a/src/Pure/type.ML	Thu Dec 14 22:19:39 2006 +0100
     1.2 +++ b/src/Pure/type.ML	Fri Dec 15 00:08:06 2006 +0100
     1.3 @@ -535,7 +535,8 @@
     1.4  fun map_types f = map_tsig (fn (classes, default, types) =>
     1.5    let
     1.6      val (space', tab') = f types;
     1.7 -    val _ = assert (NameSpace.intern space' "dummy" = "dummy") "Illegal declaration of dummy type";
     1.8 +    val _ = NameSpace.intern space' "dummy" = "dummy" orelse
     1.9 +      error "Illegal declaration of dummy type";
    1.10    in (classes, default, (space', tab')) end);
    1.11  
    1.12  fun syntactic types (Type (c, Ts)) =