src/HOL/HOLCF/Compact_Basis.thy
changeset 49834 b27bbb021df1
parent 45694 4a8743618257
child 51489 f738e6dbd844
--- a/src/HOL/HOLCF/Compact_Basis.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -14,7 +14,7 @@
 
 definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
 
-typedef (open) 'a pd_basis = "pd_basis :: 'a compact_basis set set"
+typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set"
   unfolding pd_basis_def
   apply (rule_tac x="{arbitrary}" in exI)
   apply simp