# HG changeset patch
# User wenzelm
# Date 908894137 -7200
# Node ID 39af7b3dd1c4506d56408cbaa726981877c3edb3
# Parent  998af7667fa33076e750167e29fd01cad4175bdf
Datatype instead of Prod;

diff -r 998af7667fa3 -r 39af7b3dd1c4 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 *)