diff -r 7f504136149b -r 68b2d2d7b4ed Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon May 03 14:31:11 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 03 15:13:15 2010 +0200
@@ -159,8 +159,9 @@
 end
 *}
 
-text {* What does the prep_bn code do? Cezary's Function? *}
-
+(* strip_bn_fun takes a bn function defined by the user as a union or
+   append of elements and returns those elements together with bn functions
+   applied *)
 ML {*
 fun strip_bn_fun t =
   case t of