# HG changeset patch
# User wenzelm
# Date 1350061100 -7200
# Node ID b27bbb021df16be2a7c794aec8e33928510f5a5d
# Parent  1d80798e8d8a7b4333c325a733f8f81d2490e0f6
discontinued obsolete typedef (open) syntax;

diff -r 1d80798e8d8a -r b27bbb021df1 src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -1189,7 +1189,7 @@
   \medskip The following trivial example pulls a three-element type
   into existence within the formal logical environment of HOL. *}
 
-typedef (open) three = "{(True, True), (True, False), (False, True)}"
+typedef three = "{(True, True), (True, False), (False, True)}"
   by blast
 
 definition "One = Abs_three (True, True)"
diff -r 1d80798e8d8a -r b27bbb021df1 src/Doc/Tutorial/Types/Typedefs.thy
--- a/src/Doc/Tutorial/Types/Typedefs.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/Doc/Tutorial/Types/Typedefs.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -69,7 +69,7 @@
 It is easily represented by the first three natural numbers:
 *}
 
-typedef (open) three = "{0::nat, 1, 2}"
+typedef three = "{0::nat, 1, 2}"
 
 txt{*\noindent
 In order to enforce that the representing set on the right-hand side is
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -42,7 +42,7 @@
 
 definition "UP = {f :: nat => 'a::zero. EX n. bound n f}"
 
-typedef (open) 'a up = "UP :: (nat => 'a::zero) set"
+typedef 'a up = "UP :: (nat => 'a::zero) set"
   morphisms Rep_UP Abs_UP
 proof -
   have "bound 0 (\<lambda>_. 0::'a)" by (rule boundI) (rule refl)
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/BNF/Countable_Set.thy
--- a/src/HOL/BNF/Countable_Set.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/BNF/Countable_Set.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -315,7 +315,7 @@
 
 subsection{*  The type of countable sets *}
 
-typedef (open) 'a cset = "{A :: 'a set. countable A}"
+typedef 'a cset = "{A :: 'a set. countable A}"
 apply(rule exI[of _ "{}"]) by simp
 
 abbreviation rcset where "rcset \<equiv> Rep_cset"
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -13,7 +13,7 @@
 
 subsection {* Datatype of target language numerals *}
 
-typedef (open) code_numeral = "UNIV \<Colon> nat set"
+typedef code_numeral = "UNIV \<Colon> nat set"
   morphisms nat_of of_nat ..
 
 lemma of_nat_nat_of [simp]:
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Datatype.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -14,7 +14,7 @@
 
 definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
 
-typedef (open) ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
+typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
   morphisms Rep_Node Abs_Node
   unfolding Node_def by auto
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/HOLCF/Algebraic.thy
--- 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
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/HOLCF/Compact_Basis.thy
--- 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
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -119,7 +119,7 @@
 
 subsection {* Type definition *}
 
-typedef (open) 'a convex_pd =
+typedef 'a convex_pd =
   "{S::'a pd_basis set. convex_le.ideal S}"
 by (rule convex_le.ex_ideal)
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -74,7 +74,7 @@
 
 subsection {* Type definition *}
 
-typedef (open) 'a lower_pd =
+typedef 'a lower_pd =
   "{S::'a pd_basis set. lower_le.ideal S}"
 by (rule lower_le.ex_ideal)
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/Universal.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -198,7 +198,7 @@
 
 subsection {* Defining the universal domain by ideal completion *}
 
-typedef (open) udom = "{S. udom.ideal S}"
+typedef udom = "{S. udom.ideal S}"
 by (rule udom.ex_ideal)
 
 instantiation udom :: below
@@ -247,7 +247,7 @@
 
 subsection {* Compact bases of domains *}
 
-typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}"
+typedef 'a compact_basis = "{x::'a::pcpo. compact x}"
 by auto
 
 lemma Rep_compact_basis' [simp]: "compact (Rep_compact_basis a)"
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -72,7 +72,7 @@
 
 subsection {* Type definition *}
 
-typedef (open) 'a upper_pd =
+typedef 'a upper_pd =
   "{S::'a pd_basis set. upper_le.ideal S}"
 by (rule upper_le.ex_ideal)
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Induct/QuoDataType.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -125,7 +125,7 @@
 
 definition "Msg = UNIV//msgrel"
 
-typedef (open) msg = Msg
+typedef msg = Msg
   morphisms Rep_Msg Abs_Msg
   unfolding Msg_def by (auto simp add: quotient_def)
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -144,7 +144,7 @@
 
 definition "Exp = UNIV//exprel"
 
-typedef (open) exp = Exp
+typedef exp = Exp
   morphisms Rep_Exp Abs_Exp
   unfolding Exp_def by (auto simp add: quotient_def)
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Induct/SList.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -55,7 +55,7 @@
 
 definition "List = list (range Leaf)"
 
-typedef (open) 'a list = "List :: 'a item set"
+typedef 'a list = "List :: 'a item set"
   morphisms Rep_List Abs_List
   unfolding List_def by (blast intro: list.NIL_I)
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Bit.thy
--- a/src/HOL/Library/Bit.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Bit.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -10,7 +10,7 @@
 
 subsection {* Bits as a datatype *}
 
-typedef (open) bit = "UNIV :: bool set" ..
+typedef bit = "UNIV :: bool set" ..
 
 instantiation bit :: "{zero, one}"
 begin
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/DAList.thy
--- a/src/HOL/Library/DAList.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/DAList.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -17,7 +17,7 @@
 
 subsection {* Type @{text "('key, 'value) alist" } *}
 
-typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct o map fst) xs}"
+typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct o map fst) xs}"
   morphisms impl_of Alist
 proof
   show "[] \<in> {xs. (distinct o map fst) xs}" by simp
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Dlist.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -8,7 +8,7 @@
 
 subsection {* The type of distinct lists *}
 
-typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
+typedef 'a dlist = "{xs::'a list. distinct xs}"
   morphisms list_of_dlist Abs_dlist
 proof
   show "[] \<in> {xs. distinct xs}" by simp
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -25,7 +25,7 @@
   infinity.
 *}
 
-typedef (open) enat = "UNIV :: nat option set" ..
+typedef enat = "UNIV :: nat option set" ..
  
 definition enat :: "nat \<Rightarrow> enat" where
   "enat n = Abs_enat (Some n)"
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/FinFun.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -83,7 +83,7 @@
 
 definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
 
-typedef (open) ('a,'b) finfun  ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
+typedef ('a,'b) finfun  ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
   morphisms finfun_apply Abs_finfun
 proof -
   have "\<exists>f. finite {x. f x \<noteq> undefined}"
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Float.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -11,7 +11,7 @@
 
 definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
 
-typedef (open) float = float
+typedef float = float
   morphisms real_of_float float_of
   unfolding float_def by auto
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -11,7 +11,7 @@
 
 subsection {* The type of formal power series*}
 
-typedef (open) 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
+typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
   morphisms fps_nth Abs_fps
   by simp
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Fraction_Field.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -55,7 +55,7 @@
 
 definition "fract = {(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel"
 
-typedef (open) 'a fract = "fract :: ('a * 'a::idom) set set"
+typedef 'a fract = "fract :: ('a * 'a::idom) set set"
   unfolding fract_def
 proof
   have "(0::'a, 1::'a) \<in> {x. snd x \<noteq> 0}" by simp
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Mapping.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -8,7 +8,7 @@
 
 subsection {* Type definition and primitive operations *}
 
-typedef (open) ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
+typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
   morphisms lookup Mapping ..
 
 lemma lookup_Mapping [simp]:
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -12,7 +12,7 @@
 
 definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}"
 
-typedef (open) 'a multiset = "multiset :: ('a => nat) set"
+typedef 'a multiset = "multiset :: ('a => nat) set"
   morphisms count Abs_multiset
   unfolding multiset_def
 proof
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -10,16 +10,16 @@
 
 subsection {* Numeral Types *}
 
-typedef (open) num0 = "UNIV :: nat set" ..
-typedef (open) num1 = "UNIV :: unit set" ..
+typedef num0 = "UNIV :: nat set" ..
+typedef num1 = "UNIV :: unit set" ..
 
-typedef (open) 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
+typedef 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"
 proof
   show "0 \<in> {0 ..< 2 * int CARD('a)}"
     by simp
 qed
 
-typedef (open) 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}"
+typedef 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}"
 proof
   show "0 \<in> {0 ..< 1 + 2 * int CARD('a)}"
     by simp
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Polynomial.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -13,7 +13,7 @@
 
 definition "Poly = {f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
 
-typedef (open) 'a poly = "Poly :: (nat => 'a::zero) set"
+typedef 'a poly = "Poly :: (nat => 'a::zero) set"
   morphisms coeff Abs_poly
   unfolding Poly_def by auto
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Quotient_Type.thy
--- a/src/HOL/Library/Quotient_Type.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Quotient_Type.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -60,7 +60,7 @@
 
 definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
 
-typedef (open) 'a quot = "quot :: 'a::eqv set set"
+typedef 'a quot = "quot :: 'a::eqv set set"
   unfolding quot_def by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/RBT.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -10,7 +10,7 @@
 
 subsection {* Type definition *}
 
-typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
+typedef ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
   morphisms impl_of RBT
 proof -
   have "RBT_Impl.Empty \<in> ?rbt" by simp
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Saturated.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -12,7 +12,7 @@
 
 subsection {* The type of saturated naturals *}
 
-typedef (open) ('a::len) sat = "{.. len_of TYPE('a)}"
+typedef ('a::len) sat = "{.. len_of TYPE('a)}"
   morphisms nat_of Abs_sat
   by auto
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Library/Target_Numeral.thy
--- a/src/HOL/Library/Target_Numeral.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -4,7 +4,7 @@
 
 subsection {* Type of target language numerals *}
 
-typedef (open) int = "UNIV \<Colon> int set"
+typedef int = "UNIV \<Colon> int set"
   morphisms int_of of_int ..
 
 hide_type (open) int
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Limits.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -20,7 +20,7 @@
   assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
   assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
 
-typedef (open) 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
+typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
 proof
   show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
 qed
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Matrix_LP/Matrix.thy
--- a/src/HOL/Matrix_LP/Matrix.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -13,7 +13,7 @@
 
 definition "matrix = {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
 
-typedef (open) 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
+typedef 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
   unfolding matrix_def
 proof
   show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -13,7 +13,7 @@
 
 subsection {* Finite Cartesian products, with indexing and lambdas. *}
 
-typedef (open) ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
+typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
   morphisms vec_nth vec_lambda ..
 
 notation
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -13,7 +13,7 @@
 subsection {* General notion of a topology as a value *}
 
 definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
-typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
+typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
   morphisms "openin" "topology"
   unfolding istopology_def by blast
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -40,7 +40,7 @@
 
 definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
 
-typedef (open) 'a star = "star :: (nat \<Rightarrow> 'a) set set"
+typedef 'a star = "star :: (nat \<Rightarrow> 'a) set set"
   unfolding star_def by (auto intro: quotientI)
 
 definition
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Nat.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -33,7 +33,7 @@
   Zero_RepI: "Nat Zero_Rep"
 | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
 
-typedef (open) nat = "{n. Nat n}"
+typedef nat = "{n. Nat n}"
   morphisms Rep_Nat Abs_Nat
   using Nat.Zero_RepI by auto
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -95,7 +95,7 @@
 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
 
 definition "three = {0\<Colon>nat, 1, 2}"
-typedef (open) three = three
+typedef three = three
   unfolding three_def by blast
 
 definition A :: three where "A \<equiv> Abs_three 0"
@@ -201,7 +201,7 @@
 (* BEGIN LAZY LIST SETUP *)
 definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
 
-typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
+typedef 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
 unfolding llist_def by auto
 
 definition LNil where
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -541,7 +541,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\<Colon>'a myTdef) = y"
@@ -552,7 +552,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\<Colon>(myTdecl myTdef) T_bij)"
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -15,7 +15,7 @@
                 timeout = 240]
 
 definition "three = {0\<Colon>nat, 1, 2}"
-typedef (open) three = three
+typedef three = three
 unfolding three_def by blast
 
 definition A :: three where "A \<equiv> Abs_three 0"
@@ -28,7 +28,7 @@
 
 definition "one_or_two = {undefined False\<Colon>'a, undefined True}"
 
-typedef (open) 'a one_or_two = "one_or_two :: 'a set"
+typedef 'a one_or_two = "one_or_two :: 'a set"
 unfolding one_or_two_def by auto
 
 lemma "x = (y\<Colon>unit one_or_two)"
@@ -54,7 +54,7 @@
 
 definition "bounded = {n\<Colon>nat. finite (UNIV \<Colon> 'a set) \<longrightarrow> n < card (UNIV \<Colon> 'a set)}"
 
-typedef (open) 'a bounded = "bounded(TYPE('a))"
+typedef 'a bounded = "bounded(TYPE('a))"
 unfolding bounded_def
 apply (rule_tac x = 0 in exI)
 apply (case_tac "card UNIV = 0")
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -3376,7 +3376,7 @@
 
 definition "ABS = ABS_set"
 
-typedef (open) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
+typedef ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
     "ABS::('x\<Rightarrow>('a noption)) set"
   morphisms Rep_ABS Abs_ABS
   unfolding ABS_def
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -997,7 +997,7 @@
 definition measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
   "measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
 
-typedef (open) 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
+typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
 proof
   have "sigma_algebra UNIV {{}, UNIV}"
     by (auto simp: sigma_algebra_iff2)
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Product_Type.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -43,7 +43,7 @@
 
 subsection {* The @{text unit} type *}
 
-typedef (open) unit = "{True}"
+typedef unit = "{True}"
   by auto
 
 definition Unity :: unit  ("'(')")
@@ -132,7 +132,7 @@
 
 definition "prod = {f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
 
-typedef (open) ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
+typedef ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
   unfolding prod_def by auto
 
 type_notation (xsymbols)
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -25,7 +25,7 @@
 
 subsubsection {* Type @{text "code_int"} for Haskell Quickcheck's Int type *}
 
-typedef (open) code_int = "UNIV \<Colon> int set"
+typedef code_int = "UNIV \<Colon> int set"
   morphisms int_of of_int by rule
 
 lemma of_int_int_of [simp]:
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Quotient_Examples/Lift_DList.thy
--- a/src/HOL/Quotient_Examples/Lift_DList.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -8,7 +8,7 @@
 
 subsection {* The type of distinct lists *}
 
-typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
+typedef 'a dlist = "{xs::'a list. distinct xs}"
   morphisms list_of_dlist Abs_dlist
 proof
   show "[] \<in> {xs. distinct xs}" by simp
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Quotient_Examples/Lift_Set.thy
--- a/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -10,7 +10,7 @@
 
 definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
 
-typedef (open) 'a set = "set :: ('a \<Rightarrow> bool) set"
+typedef 'a set = "set :: ('a \<Rightarrow> bool) set"
   morphisms member Set
   unfolding set_def by auto
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -760,7 +760,7 @@
 
 definition "three = {1, 2, 3::int}"
 
-typedef (open) three = three
+typedef three = three
   unfolding three_def by auto
 
 definition n1 where "n1 = Abs_three 1"
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/String.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -152,7 +152,7 @@
 
 subsection {* Strings as dedicated type *}
 
-typedef (open) literal = "UNIV :: string set"
+typedef literal = "UNIV :: string set"
   morphisms explode STR ..
 
 instantiation literal :: size
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Sum_Type.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -19,7 +19,7 @@
 
 definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
 
-typedef (open) ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set"
+typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set"
   unfolding sum_def by auto
 
 lemma Inl_RepI: "Inl_Rep a \<in> sum"
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Tools/typedef.ML	Fri Oct 12 18:58:20 2012 +0200
@@ -276,17 +276,12 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
     "HOL type definition (requires non-emptiness proof)"
-    (Scan.optional (@{keyword "("} |--
-        ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
-          Parse.binding >> (fn s => (true, SOME s))) --| @{keyword ")"}) (true, NONE) --
+    (Scan.option (@{keyword "("} |-- Parse.binding --| @{keyword ")"}) --
       (Parse.type_args_constrained -- Parse.binding) --
         Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
         Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
-    >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => fn lthy =>
-          (if def then
-            error "typedef with implicit set definition -- use \"typedef (open)\" instead"
-           else ();
-           typedef_cmd (the_default t opt_name, (t, args, mx), A, morphs) lthy)));
+    >> (fn (((((opt_name, (args, t)), mx), A), morphs)) => fn lthy =>
+           typedef_cmd (the_default t opt_name, (t, args, mx), A, morphs) lthy));
 
 end;
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/UNITY/UNITY.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -17,7 +17,7 @@
     {(init:: 'a set, acts :: ('a * 'a)set set,
       allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}"
 
-typedef (open) 'a program = "Program :: ('a set * ('a * 'a) set set * ('a * 'a) set set) set"
+typedef 'a program = "Program :: ('a set * ('a * 'a) set set * ('a * 'a) set set) set"
   morphisms Rep_Program Abs_Program
   unfolding Program_def by blast
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Word/Word.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -16,7 +16,7 @@
 
 subsection {* Type definition *}
 
-typedef (open) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
+typedef 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
   morphisms uint Abs_word by auto
 
 lemma uint_nonnegative:
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ZF/Games.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -191,7 +191,7 @@
 
 definition "game = games_lfp"
 
-typedef (open) game = game
+typedef game = game
   unfolding game_def by (blast intro: games_lfp_nonempty)
 
 definition left_options :: "game \<Rightarrow> game zet" where
@@ -843,7 +843,7 @@
 
 definition "Pg = UNIV//eq_game_rel"
 
-typedef (open) Pg = Pg
+typedef Pg = Pg
   unfolding Pg_def by (auto simp add: quotient_def)
 
 lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/ZF/Zet.thy
--- a/src/HOL/ZF/Zet.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ZF/Zet.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -11,7 +11,7 @@
 
 definition "zet = {A :: 'a set | A f z. inj_on f A \<and> f ` A \<subseteq> explode z}"
 
-typedef (open) 'a zet = "zet :: 'a set set"
+typedef 'a zet = "zet :: 'a set set"
   unfolding zet_def by blast
 
 definition zin :: "'a \<Rightarrow> 'a zet \<Rightarrow> bool" where
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -46,7 +46,7 @@
 
 definition "preal = {A. cut A}"
 
-typedef (open) preal = preal
+typedef preal = preal
   unfolding preal_def by (blast intro: cut_of_rat [OF zero_less_one])
 
 definition
@@ -1171,7 +1171,7 @@
 
 definition "Real = UNIV//realrel"
 
-typedef (open) real = Real
+typedef real = Real
   morphisms Rep_Real Abs_Real
   unfolding Real_def by (auto simp add: quotient_def)
 
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/ex/Executable_Relation.thy
--- a/src/HOL/ex/Executable_Relation.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ex/Executable_Relation.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -6,7 +6,7 @@
 
 subsubsection {* Definition of the dedicated type for relations *}
 
-typedef (open) 'a rel = "UNIV :: (('a * 'a) set) set"
+typedef 'a rel = "UNIV :: (('a * 'a) set) set"
 morphisms set_of_rel rel_of_set by simp
 
 setup_lifting type_definition_rel
diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/ex/PER.thy
--- a/src/HOL/ex/PER.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ex/PER.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -153,7 +153,7 @@
 
 definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
 
-typedef (open) 'a quot = "quot :: 'a::partial_equiv set set"
+typedef 'a quot = "quot :: 'a::partial_equiv set set"
   unfolding quot_def by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
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)"