# HG changeset patch
# User wenzelm
# Date 898187707 -7200
# Node ID bbe3584b515b902491e124e869ba21586326a21f
# Parent  3b45aee5c7ecdf4873bfed7f6a2cc476f8167f06
fixed comment;

diff -r 3b45aee5c7ec -r bbe3584b515b src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Jun 18 18:31:06 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Thu Jun 18 18:35:07 1998 +0200
@@ -256,7 +256,7 @@
   simps: tthm list};
 
 
-(* data kind '"HOL/records' *)
+(* data kind 'HOL/records' *)
 
 structure RecordsArgs =
 struct