# HG changeset patch
# User wenzelm
# Date 860751231 -7200
# Node ID bd922fc9001bc769e4e51a0edca56a8cb46683ff
# Parent  f842a75d96246ec37c9ed6abc5d2e1b181833519
tuned error msg;

diff -r f842a75d9624 -r bd922fc9001b 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 *)