1.1 --- a/src/HOL/ex/Records.thy	Fri Dec 21 23:18:27 2001 +0100
     1.2 +++ b/src/HOL/ex/Records.thy	Fri Dec 21 23:18:46 2001 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4  lemma "r = (| xpos = xpos r, ypos = ypos r |)"
     1.5    by simp
     1.6  
     1.7 -lemma "r = (| xpos = xpos r, ypos = ypos r, ... = more r |)"
     1.8 +lemma "r = (| xpos = xpos r, ypos = ypos r, ... = point.more r |)"
     1.9    by simp
    1.10  
    1.11