--- a/src/HOL/NSA/StarDef.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/NSA/StarDef.thy Wed Nov 30 16:27:10 2011 +0100
@@ -39,8 +39,10 @@
starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where
"starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}"
-typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
-by (auto intro: quotientI)
+definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
+
+typedef (open) 'a star = "star :: (nat \<Rightarrow> 'a) set set"
+ unfolding star_def by (auto intro: quotientI)
definition
star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star" where