# HG changeset patch
# User berghofe
# Date 1175010877 -7200
# Node ID 902ed60d53a75bdf6ce572ab29cc45626a6df368
# Parent  8501c4a62a3c4daf85a1ca54aea8af13e520b5d1
Exported perm_of_pair, mk_not_sym, and perm_simproc.

diff -r 8501c4a62a3c -r 902ed60d53a7 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Mar 27 12:28:42 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Mar 27 17:54:37 2007 +0200
@@ -14,6 +14,9 @@
   val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
   val get_nominal_datatype : theory -> string -> nominal_datatype_info option
   val mk_perm: typ list -> term -> term -> term
+  val perm_of_pair: term * term -> term
+  val mk_not_sym: thm list -> thm list
+  val perm_simproc: simproc
   val setup: theory -> theory
 end
 
@@ -220,6 +223,18 @@
     val U = fastype_of1 (Ts, u)
   in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
 
+fun perm_of_pair (x, y) =
+  let
+    val T = fastype_of x;
+    val pT = mk_permT T
+  in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
+    HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
+  end;
+
+fun mk_not_sym ths = maps (fn th => case prop_of th of
+    _ $ (Const ("Not", _) $ _) => [th, th RS not_sym]
+  | _ => [th]) ths;
+
 fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
   let
     (* this theory is used just for parsing *)
@@ -1592,14 +1607,6 @@
     val perm_fresh_fresh = PureThy.get_thms thy11 (Name "perm_fresh_fresh");
     val perm_swap = PureThy.get_thms thy11 (Name "perm_swap");
 
-    fun perm_of_pair (x, y) =
-      let
-        val T = fastype_of x;
-        val pT = mk_permT T
-      in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
-        HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
-      end;
-
     val finite_premss = map (fn aT =>
       map (fn (f, T) => HOLogic.mk_Trueprop
         (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
@@ -1798,10 +1805,6 @@
                     val pi2 = map perm_of_pair (boundsr ~~ freshs1);
                     val rpi2 = rev pi2;
 
-                    fun mk_not_sym ths = List.concat (map (fn th =>
-                      case prop_of th of
-                          _ $ (Const ("Not", _) $ _) => [th, th RS not_sym]
-                        | _ => [th]) ths);
                     val fresh_prems' = mk_not_sym fresh_prems;
                     val freshs2' = mk_not_sym freshs2;