tuned error msg;
authorwenzelm
Fri, 11 Apr 1997 11:33:51 +0200
changeset 2934 bd922fc9001b
parent 2933 f842a75d9624
child 2935 998cb95fdd43
tuned error msg;
src/HOL/typedef.ML
--- a/src/HOL/typedef.ML	Thu Apr 10 18:07:27 1997 +0200
+++ b/src/HOL/typedef.ML	Fri Apr 11 11:33:51 1997 +0200
@@ -38,7 +38,7 @@
     prove_goalw_cterm [] goal (K [tac])
   end
   handle ERROR =>
-    error ("Failed to prove non-emptyness of " ^ quote (string_of_cterm cset));
+    error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset));
 
 
 (* ext_typedef *)