--- a/src/HOL/Bali/Name.thy Sun Aug 28 16:04:43 2005 +0200
+++ b/src/HOL/Bali/Name.thy Sun Aug 28 16:04:44 2005 +0200
@@ -13,14 +13,6 @@
typedecl vname --{* variable or field name *}
typedecl label --{* label as destination of break or continue *}
-arities
- tnam :: "type"
- pname :: "type"
- vname :: "type"
- mname :: "type"
- label :: "type"
-
-
datatype ename --{* expression name *}
= VNam vname
| Res --{* special name to model the return value of methods *}
@@ -75,11 +67,10 @@
defs (overloaded)
tname_tname_def: "tname (t::tname) \<equiv> t"
-axclass has_qtname < "type"
+axclass has_qtname < type
consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
-(* Declare qtname as instance of has_qtname *)
-instance qtname_ext_type::("type") has_qtname ..
+instance qtname_ext_type :: (type) has_qtname ..
defs (overloaded)
qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
@@ -108,4 +99,3 @@
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
by (simp add: SXcpt_def)
end
-