--- a/Nominal/Fv.thy	Thu Mar 18 11:37:10 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 18 12:09:59 2010 +0100
@@ -33,7 +33,7 @@
 *)
 
 (*
-The overview of the generation of free variables:
+An overview of the generation of free variables:
 
 1) fv_bn functions are generated only for the non-recursive binds.
 
@@ -76,6 +76,10 @@
    - for nominal datatype ty' return: fv_ty' x
 *)
 
+(*
+An overview of the generation of alpha-equivalence:
+*)
+
 ML {*
 fun is_atom thy typ =
   Sign.of_sort thy (typ, @{sort at})