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