# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271606325 -7200
# Node ID c704d129862bf888fba2de56b1202fb9c4d3053f
# Parent  55b2da92ff2febd33782beced4a7ff3771f85770
moved some general function into nominal_library.ML

diff -r 55b2da92ff2f -r c704d129862b Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Sun Apr 18 17:57:27 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Sun Apr 18 17:58:45 2010 +0200
@@ -7,6 +7,7 @@
 signature NOMINAL_LIBRARY =
 sig
   val mk_minus: term -> term
+  val mk_perm_ty: typ -> term -> term -> term
   val mk_perm: term -> term -> term
   val dest_perm: term -> term * term
 
@@ -21,12 +22,10 @@
 fun mk_minus p = 
  Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p
 
-fun mk_perm p trm =
-let
-  val ty = fastype_of trm
-in
+fun mk_perm_ty ty p trm =
   Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
-end
+
+fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM ("dest_perm", [t])
diff -r 55b2da92ff2f -r c704d129862b Nominal/Perm.thy
--- a/Nominal/Perm.thy	Sun Apr 18 17:57:27 2010 +0200
+++ b/Nominal/Perm.thy	Sun Apr 18 17:58:45 2010 +0200
@@ -4,8 +4,7 @@
 
 ML {*
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *)
-  fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);
-  val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
+  open Nominal_Library; 
 *}
 
 ML {*
@@ -94,10 +93,10 @@
             in list_abs (map (pair "x") Us,
               Free (nth perm_names_types' (body_index dt)) $ pi $
                 list_comb (x, map (fn (i, U) =>
-                  (permute U) $ (minus_perm $ pi) $ Bound i)
+                  (mk_perm_ty U (mk_minus pi) (Bound i)))
                   ((length Us - 1 downto 0) ~~ Us)))
             end
-          else (permute T) $ pi $ x
+          else (mk_perm_ty T pi x)
         end;
     in
       (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -125,7 +124,8 @@
   lthy'
   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))
   |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
-  |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
+  |> Class_Target.prove_instantiation_exit_result morphism tac 
+      (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
   end
 
 *}