comment modified

--- a/src/HOL/ex/Refute_Examples.thy	Tue Aug 24 17:55:24 2004 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Thu Aug 26 17:28:57 2004 +0200
@@ -455,8 +455,9 @@
 
 subsection {* Subtypes (typedef), typedecl *}
 
+text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
+
 typedef 'a myTdef = "insert (arbitrary::'a) (arbitrary::'a set)"
-  -- {* a completely unspecified non-empty subset of @{typ "'a"} *}
   by auto
 
 lemma "(x::'a myTdef) = y"