# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271277682 -7200
# Node ID 756982b4fe20bf62df17dacacc5020bc73cb33a1
# Parent  b7423c6b55645a5b6d52cf85400cd4d85ceafa14
temporary fix for CoreHaskell

diff -r b7423c6b5564 -r 756982b4fe20 Nominal-General/nominal_thmdecls.ML
--- 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 =
diff -r b7423c6b5564 -r 756982b4fe20 Nominal/Ex/ExCoreHaskell.thy
--- 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