# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271250127 -7200
# Node ID 9909cc3566c5a092adc21c6e9151b52b19621203
# Parent  2050b5723c044cfa3385adfca6d905773c93840e
moved a couple of more functions to the library

diff -r 2050b5723c04 -r 9909cc3566c5 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Wed Apr 14 14:41:54 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Wed Apr 14 15:02:07 2010 +0200
@@ -8,6 +8,10 @@
 sig
   val mk_minus: term -> term
   val mk_perm: term -> term -> term
+  val dest_perm: term -> term * term
+
+  val mk_equiv: thm -> thm
+  val safe_mk_equiv: thm -> thm
 end
 
 
@@ -24,7 +28,11 @@
   Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
 end
 
+fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
+  | dest_perm t = raise TERM ("dest_perm", [t])
 
+fun mk_equiv r = r RS @{thm eq_reflection};
+fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
 end (* structure *)
 
diff -r 2050b5723c04 -r 9909cc3566c5 Nominal-General/nominal_permeq.ML
--- a/Nominal-General/nominal_permeq.ML	Wed Apr 14 14:41:54 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Wed Apr 14 15:02:07 2010 +0200
@@ -120,9 +120,6 @@
   Conv.all_conv ctrm 
 end
 
-fun mk_equiv r = r RS @{thm eq_reflection};
-fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
-
 (* main conversion *)
 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
 let
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