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]: