diff -r 01c4d19f597e -r 87ad6e8a5f2c src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Sun Jun 03 23:16:46 2007 +0200
+++ b/src/HOL/ex/LocaleTest2.thy	Sun Jun 03 23:16:47 2007 +0200
@@ -19,7 +19,8 @@
 ML {* set show_hyps *}
 ML {* set show_sorts *}
 
-section {* Interpretation of Defined Concepts *}
+
+subsection {* Interpretation of Defined Concepts *}
 
 text {* Naming convention for global objects: prefixes D and d *}