src/HOL/Bali/Name.thy
changeset 35315 fbdc860d87a3
parent 35069 09154b995ed8
child 35431 8758fe1fc9f8
--- 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"