diff -r 731b27c90d2f -r 76caebd18756 src/LK/LK.thy
--- a/src/LK/LK.thy	Thu Mar 17 13:54:50 1994 +0100
+++ b/src/LK/LK.thy	Thu Mar 17 17:48:37 1994 +0100
@@ -7,11 +7,17 @@
 *)
 
 LK = Pure +
+
 classes term < logic
+
 default term
-types o 0
-      sequence,seqobj,seqcont,sequ,sobj 0
-arities o :: logic
+
+types
+ o sequence seqobj seqcont sequ sobj
+
+arities
+ o :: logic
+
 consts
  True,False	:: "o"
  "="		:: "['a,'a] => o"	(infixl 50)