--- a/src/HOL/HOLCF/Compact_Basis.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy Wed Nov 30 16:27:10 2011 +0100
@@ -12,9 +12,13 @@
subsection {* A compact basis for powerdomains *}
-typedef 'a pd_basis =
- "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
-by (rule_tac x="{arbitrary}" in exI, simp)
+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"
+ unfolding pd_basis_def
+ apply (rule_tac x="{arbitrary}" in exI)
+ apply simp
+ done
lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp