--- a/Nominal/Ex/ExCoreHaskell.thy	Wed Apr 14 22:23:52 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy	Wed Apr 14 22:41:22 2010 +0200
@@ -6,8 +6,10 @@
 
 ML {* val _ = recursive := false *}
 (* this should not be a raw equivariant rule *)
-declare permute_pure[eqvt]
-
+(* we force it to be                         *)
+setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
+thm eqvts
+(*declare permute_pure[eqvt]*)
 
 atom_decl var
 atom_decl cvar