diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -485,7 +485,7 @@
 
 definition "myTdef = insert (undefined::'a) (undefined::'a set)"
 
-typedef (open) 'a myTdef = "myTdef :: 'a set"
+typedef 'a myTdef = "myTdef :: 'a set"
   unfolding myTdef_def by auto
 
 lemma "(x::'a myTdef) = y"
@@ -496,7 +496,7 @@
 
 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"
+typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
   unfolding T_bij_def by auto
 
 lemma "P (f::(myTdecl myTdef) T_bij)"