--- a/Quot/Nominal/Perm.thy	Wed Feb 24 18:38:49 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Wed Feb 24 23:25:30 2010 +0100
@@ -13,13 +13,11 @@
 let
   val perm_types = map fastype_of perm_frees;
   val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
+  fun glc ((perm, T), x) =
+    HOLogic.mk_eq (perm $ @{term "0 :: perm"} $ Free (x, T), Free (x, T))
   val gl =
     HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map (fn ((perm, T), x) => HOLogic.mk_eq
-          (perm $ @{term "0 :: perm"} $ Free (x, T),
-           Free (x, T)))
-       (perm_frees ~~
-        map body_type perm_types ~~ perm_indnames)));
+      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)));
   fun tac _ =
     EVERY [
       indtac induct perm_indnames 1,
@@ -38,15 +36,13 @@
   val pi2 = Free ("pi2", @{typ perm});
   val perm_types = map fastype_of perm_frees
   val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
+  fun glc ((perm, T), x) =
+    HOLogic.mk_eq (
+      perm $ (add_perm $ pi1 $ pi2) $ Free (x, T),
+      perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
   val gl =
     (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map (fn ((perm, T), x) =>
-          let
-            val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)
-            val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))
-          in HOLogic.mk_eq (lhs, rhs)
-          end)
-        (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
+      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
   fun tac _ =
     EVERY [
       indtac induct perm_indnames 1,