diff -r e25b0fff0dd2 -r 409ecb7284dd Nominal/Perm.thy
--- a/Nominal/Perm.thy	Tue May 11 18:20:25 2010 +0200
+++ b/Nominal/Perm.thy	Wed May 12 13:43:48 2010 +0100
@@ -62,6 +62,7 @@
 *}
 
 ML {*
+(* proves the two pt-type class properties *)
 fun prove_permute_zero lthy induct perm_defs perm_fns =
 let
   val perm_types = map (body_type o fastype_of) perm_fns