src/HOL/Set.thy
changeset 12338 de0f4a63baa5
parent 12257 e3f7d6fb55d7
child 12633 ad9277743664
--- a/src/HOL/Set.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Set.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -17,7 +17,7 @@
 global
 
 typedecl 'a set
-arities set :: ("term") "term"
+arities set :: (type) type
 
 consts
   "{}"          :: "'a set"                             ("{}")
@@ -42,8 +42,8 @@
 
 local
 
-instance set :: ("term") ord ..
-instance set :: ("term") minus ..
+instance set :: (type) ord ..
+instance set :: (type) minus ..
 
 
 subsection {* Additional concrete syntax *}