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 =