diff -r 54ad41f9e505 -r 996d4411e95e Nominal/Fv.thy
--- a/Nominal/Fv.thy	Mon Apr 19 15:37:54 2010 +0200
+++ b/Nominal/Fv.thy	Mon Apr 19 16:55:36 2010 +0200
@@ -274,7 +274,6 @@
 end;
 *}
 
-ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
 
 ML {*
 fun non_rec_binds l =
@@ -596,7 +595,7 @@
                 val fv = mk_compound_fv fvs;
                 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos);
                 val alpha = mk_compound_alpha alphas;
-                val pi = foldr1 add_perm (distinct (op =) rpis);
+                val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis);
                 val alpha_gen_pre = Const (atyp_const atyp, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
                 val alpha_gen = Syntax.check_term lthy alpha_gen_pre
               in
@@ -618,7 +617,7 @@
               val rhs = mk_pair (rhs_binds, arg2);
               val alpha = nth alpha_frees (body_index dt);
               val fv = nth fv_frees (body_index dt);
-              val pi = foldr1 add_perm (distinct (op =) rpis);
+              val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis);
               val alpha_const = alpha_const_for_binds rbinds;
               val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
               val alpha_gen = Syntax.check_term lthy alpha_gen_pre