removed obsolete arities;
authorwenzelm
Sun, 28 Aug 2005 16:04:44 +0200
changeset 17160 fb65eda72fc7
parent 17159 d5060118122e
child 17161 57c69627d71a
removed obsolete arities;
src/HOL/Bali/Name.thy
src/HOL/Bali/Value.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
-
--- 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 *}