src/HOL/Record.thy

--- a/src/HOL/Record.thy	Tue Oct 20 16:33:47 1998 +0200
+++ b/src/HOL/Record.thy	Tue Oct 20 16:35:37 1998 +0200
@@ -6,7 +6,7 @@
 Tools/record_package.ML for the actual implementation.
 *)
 
-Record = Prod +
+Record = Datatype +
 
 
 (* concrete syntax *)
@@ -43,9 +43,7 @@
 (* type class for record extensions *)
 
 axclass more < term
-
 instance unit :: more
-instance "*" :: (term, more) more
 
 
 (* initialize the package *)