diff -r 3573830e9b91 -r 5a46569d2b05 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Fri Dec 21 23:18:27 2001 +0100
+++ b/src/HOL/ex/Records.thy	Fri Dec 21 23:18:46 2001 +0100
@@ -98,7 +98,7 @@
 lemma "r = (| xpos = xpos r, ypos = ypos r |)"
   by simp
 
-lemma "r = (| xpos = xpos r, ypos = ypos r, ... = more r |)"
+lemma "r = (| xpos = xpos r, ypos = ypos r, ... = point.more r |)"
   by simp