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