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 =