--- a/Nominal/Ex/ExCoreHaskell.thy	Fri Apr 16 16:29:11 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy	Sun Apr 18 09:26:38 2010 +0200
@@ -5,8 +5,8 @@
 (* core haskell *)
 
 ML {* val _ = recursive := false *}
-(* this should not be a raw equivariant rule *)
-(* we force it to be                         *)
+(* this should not be an equivariance rule *)
+(* for the moment, we force it to be       *)
 setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
 thm eqvts
 (*declare permute_pure[eqvt]*)