diff -r d33781f9d2c7 -r d3b89f6c086a Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sat Apr 24 09:49:23 2010 +0200 +++ b/Nominal/NewParser.thy Sat Apr 24 10:00:33 2010 +0200 @@ -191,7 +191,7 @@ end *} -text {* What does the prep_bn code do ? *} +text {* What does the prep_bn code do? Cezary's Function? *} ML {* fun strip_bn_fun t =