# HG changeset patch
# User wenzelm
# Date 1008973126 -3600
# Node ID 5a46569d2b05276c6b8e2c175c38278fb493953b
# Parent  3573830e9b918150afb8424aa02d8e50977b7543
qualified point.more;

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