--- a/Nominal-General/nominal_thmdecls.ML	Wed Apr 14 22:23:52 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Wed Apr 14 22:41:22 2010 +0200
@@ -34,6 +34,9 @@
   val get_eqvts_thms: Proof.context -> thm list
   val get_eqvts_raw_thms: Proof.context -> thm list
 
+  (* TEMPORARY FIX *)
+  val add_thm: thm -> Context.generic -> Context.generic
+  val add_raw_thm: thm -> Context.generic -> Context.generic
 end;
 
 structure Nominal_ThmDecls: NOMINAL_THMDECLS =

--- 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