diff -r 9909cc3566c5 -r 636de31888a6 Nominal-General/nominal_thmdecls.ML
--- a/Nominal-General/nominal_thmdecls.ML	Wed Apr 14 15:02:07 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Wed Apr 14 16:05:58 2010 +0200
@@ -60,9 +60,6 @@
 val add_thm = EqvtData.map o Item_Net.update;
 val del_thm = EqvtData.map o Item_Net.remove;
 
-fun is_equiv (Const ("==", _) $ _ $ _) = true
-  | is_equiv _ = false
-
 fun add_raw_thm thm = 
   case prop_of thm of
     Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm)