src/HOL/Tools/record_package.ML

--- a/src/HOL/Tools/record_package.ML	Thu Feb 24 16:00:09 2000 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Feb 24 16:00:28 2000 +0100
@@ -78,6 +78,7 @@
 
 (** name components **)
 
+val recordN = "record";
 val moreN = "more";
 val schemeN = "_scheme";
 val fieldN = "_field";
@@ -659,8 +660,6 @@
 
     (* basic components *)
 
-    val rN = "r";
-
     val alphas = map fst args;
     val name = Sign.full_name sign bname;       (*not made part of record name space!*)
 
@@ -668,7 +667,7 @@
     val parent_names = map fst parent_fields;
     val parent_types = map snd parent_fields;
     val parent_len = length parent_fields;
-    val parent_xs = variantlist (map (base o fst) parent_fields, [moreN, rN]);
+    val parent_xs = variantlist (map (base o fst) parent_fields, [moreN, recordN]);
     val parent_vars = ListPair.map Free (parent_xs, parent_types);
     val parent_named_vars = parent_names ~~ parent_vars;
 
@@ -676,7 +675,7 @@
     val names = map fst fields;
     val types = map snd fields;
     val len = length fields;
-    val xs = variantlist (map fst bfields, moreN :: rN :: parent_xs);
+    val xs = variantlist (map fst bfields, moreN :: recordN :: parent_xs);
     val vars = ListPair.map Free (xs, types);
     val named_vars = names ~~ vars;
 
@@ -700,7 +699,7 @@
 
     val rec_schemeT = mk_recordT (all_fields, moreT);
     val rec_scheme = mk_record (all_named_vars, more);
-    val r = Free (rN, rec_schemeT);
+    val r = Free (recordN, rec_schemeT);
     val recT = mk_recordT (all_fields, HOLogic.unitT);