# HG changeset patch # User Christian Urban # Date 1273759925 -3600 # Node ID 2f39ce2aba6c25ac69e674057eee9f47573d3e82 # Parent 24ca435ead1477fe2e5ca094881914388d919708 removed internal functions from the signature (they are not needed anymore) 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 =