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
 
 *}