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