diff -r 2050b5723c04 -r 9909cc3566c5 Nominal-General/nominal_thmdecls.ML
--- a/Nominal-General/nominal_thmdecls.ML	Wed Apr 14 14:41:54 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Wed Apr 14 15:02:07 2010 +0200
@@ -70,16 +70,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 +103,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 +143,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