--- a/src/LCF/LCF.thy Mon Feb 10 14:33:47 2014 +0100
+++ b/src/LCF/LCF.thy Mon Feb 10 17:20:11 2014 +0100
@@ -13,7 +13,7 @@
subsection {* Natural Deduction Rules for LCF *}
-classes cpo < "term"
+class cpo = "term"
default_sort cpo
typedecl tr
@@ -21,12 +21,11 @@
typedecl ('a,'b) prod (infixl "*" 6)
typedecl ('a,'b) sum (infixl "+" 5)
-arities
- "fun" :: (cpo, cpo) cpo
- prod :: (cpo, cpo) cpo
- sum :: (cpo, cpo) cpo
- tr :: cpo
- void :: cpo
+instance "fun" :: (cpo, cpo) cpo ..
+instance prod :: (cpo, cpo) cpo ..
+instance sum :: (cpo, cpo) cpo ..
+instance tr :: cpo ..
+instance void :: cpo ..
consts
UU :: "'a"