Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/type.ML
changeset 21858 05f57309170c
parent 21116 be58cded79da
child 21934 ba683b0b2456 
--- a/src/Pure/type.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/type.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -535,7 +535,8 @@
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let
     val (space', tab') = f types;
-    val _ = assert (NameSpace.intern space' "dummy" = "dummy") "Illegal declaration of dummy type";
+    val _ = NameSpace.intern space' "dummy" = "dummy" orelse
+      error "Illegal declaration of dummy type";
   in (classes, default, (space', tab')) end);
 
 fun syntactic types (Type (c, Ts)) =
isabelle