--- a/Nominal-General/nominal_thmdecls.ML	Wed Apr 14 16:10:44 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Wed Apr 14 16:11:04 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)
@@ -70,16 +67,6 @@
 
 val del_raw_thm = EqvtRawData.map o Item_Net.remove;
 
-fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
-  | dest_perm t = raise TERM ("dest_perm", [t])
-
-fun mk_perm p trm =
-let
-  val ty = fastype_of trm
-in
-  Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
-end
-
 fun eq_transform_tac thm = REPEAT o FIRST' 
   [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}),
    rtac (thm RS @{thm trans}),
@@ -113,8 +100,6 @@
   | is_bad_list [_] = false
   | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true
 
-fun mk_minus p = 
- Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p   
 
 fun imp_transform_tac thy p p' thm = 
 let
@@ -155,9 +140,6 @@
     end
 end     
 
-fun mk_equiv r = r RS @{thm eq_reflection};
-fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
-
 fun transform addel_fun thm context = 
 let
   val ctxt = Context.proof_of context