--- a/Nominal/Test.thy	Tue Mar 23 07:04:14 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 07:04:27 2010 +0100
@@ -2,8 +2,6 @@
 imports "Parser" "../Attic/Prove"
 begin
 
-text {* example 1, equivalent to example 2 from Terms *}
-
 atom_decl name
 
 ML {* val _ = recursive := false *}
@@ -89,6 +87,8 @@
   then show "P c lm" by simp
 qed
 
+text {* example 1, equivalent to example 2 from Terms *}
+
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"