diff -r 24ca435ead14 -r 2f39ce2aba6c Nominal-General/nominal_thmdecls.ML
--- a/Nominal-General/nominal_thmdecls.ML	Thu May 13 10:34:59 2010 +0100
+++ b/Nominal-General/nominal_thmdecls.ML	Thu May 13 15:12:05 2010 +0100
@@ -35,10 +35,6 @@
   val get_eqvts_raw_thms: Proof.context -> thm list
   val eqvt_transform: Proof.context -> thm -> thm
   val is_eqvt: Proof.context -> term -> bool
-
-  (* 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 =