# HG changeset patch
# User wenzelm
# Date 1125237884 -7200
# Node ID fb65eda72fc7b9d6429d29cc1ca658b7e72111e2
# Parent  d5060118122e5d6479fe0466a100a1c22f84a766
removed obsolete arities;

diff -r d5060118122e -r fb65eda72fc7 src/HOL/Bali/Name.thy
--- 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
-
diff -r d5060118122e -r fb65eda72fc7 src/HOL/Bali/Value.thy
--- a/src/HOL/Bali/Value.thy	Sun Aug 28 16:04:43 2005 +0200
+++ b/src/HOL/Bali/Value.thy	Sun Aug 28 16:04:44 2005 +0200
@@ -9,7 +9,6 @@
 theory Value imports Type begin
 
 typedecl loc            --{* locations, i.e. abstract references on objects *}
-arities	 loc :: "type"
 
 datatype val
 	= Unit          --{* dummy result value of void methods *}