--- a/src/HOL/ex/Refute_Examples.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Wed Nov 30 16:27:10 2011 +0100
@@ -494,8 +494,10 @@
text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
-typedef 'a myTdef = "insert (undefined::'a) (undefined::'a set)"
- by auto
+definition "myTdef = insert (undefined::'a) (undefined::'a set)"
+
+typedef (open) 'a myTdef = "myTdef :: 'a set"
+ unfolding myTdef_def by auto
lemma "(x::'a myTdef) = y"
refute
@@ -503,8 +505,10 @@
typedecl myTdecl
-typedef 'a T_bij = "{(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
- by auto
+definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
+
+typedef (open) 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
+ unfolding T_bij_def by auto
lemma "P (f::(myTdecl myTdef) T_bij)"
refute