diff -r 9e9feb5f15dc -r 30e80f028c57 ex/Term.thy
--- a/ex/Term.thy	Tue May 03 11:30:09 1994 +0200
+++ b/ex/Term.thy	Tue May 03 15:48:19 1994 +0200
@@ -10,8 +10,11 @@
 *)
 
 Term = List +
-types term 1
+
+types   'a term
+
 arities term :: (term)term
+
 consts
   Term		:: "'a node set set => 'a node set set"
   Rep_Term	:: "'a term => 'a node set"
@@ -22,6 +25,7 @@
   Term_rec	::
     "['a node set, ['a node set , 'a node set, 'b list]=>'b] => 'b"
   term_rec	:: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
+
 rules
   Term_def		"Term(A) == lfp(%Z.  A <*> List(Z))"
     (*faking a type definition for term...*)