--- a/src/HOL/Bali/Name.thy Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Bali/Name.thy Tue Feb 23 10:11:12 2010 +0100
@@ -48,29 +48,34 @@
pid :: pname
tid :: tname
-axclass has_pname < "type"
-consts pname::"'a::has_pname \<Rightarrow> pname"
+class has_pname =
+ fixes pname :: "'a \<Rightarrow> pname"
-instance pname::has_pname ..
+instantiation pname :: has_pname
+begin
-defs (overloaded)
-pname_pname_def: "pname (p::pname) \<equiv> p"
+definition
+ pname_pname_def: "pname (p::pname) \<equiv> p"
-axclass has_tname < "type"
-consts tname::"'a::has_tname \<Rightarrow> tname"
+instance ..
+
+end
-instance tname::has_tname ..
+class has_tname =
+ fixes tname :: "'a \<Rightarrow> tname"
-defs (overloaded)
-tname_tname_def: "tname (t::tname) \<equiv> t"
+instantiation tname :: has_tname
+begin
-axclass has_qtname < type
-consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
+definition
+ tname_tname_def: "tname (t::tname) \<equiv> t"
+
+instance ..
-instance qtname_ext_type :: (type) has_qtname ..
+end
-defs (overloaded)
-qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
+definition
+ qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
translations
"mname" <= "Name.mname"