--- a/src/HOL/HOLCF/Algebraic.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/Algebraic.thy Fri Oct 12 18:58:20 2012 +0200
@@ -12,7 +12,7 @@
subsection {* Type constructor for finite deflations *}
-typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
+typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
by (fast intro: finite_deflation_bottom)
instantiation fin_defl :: (bifinite) below
@@ -74,7 +74,7 @@
subsection {* Defining algebraic deflations by ideal completion *}
-typedef (open) 'a defl = "{S::'a fin_defl set. below.ideal S}"
+typedef 'a defl = "{S::'a fin_defl set. below.ideal S}"
by (rule below.ex_ideal)
instantiation defl :: (bifinite) below