diff -r 874abb8aa65b -r 01386eb4eab0 src/HOL/ex/Points.thy
--- a/src/HOL/ex/Points.thy	Tue Oct 05 18:16:53 1999 +0200
+++ b/src/HOL/ex/Points.thy	Tue Oct 05 18:26:34 1999 +0200
@@ -5,7 +5,7 @@
 
 theory Points = Main:;
 
-title {* Basic use of extensible records in HOL, including the famous points
+text {* Basic use of extensible records in HOL, including the famous points
  and coloured points. *};