Nominal-General/nominal_thmdecls.ML
changeset 1846 756982b4fe20
parent 1841 fcc660ece040
child 1870 55b2da92ff2f
--- 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 =