diff -r 37d9cc4b8abf -r fe0a31cf30a0 Quot/Nominal/Perm.thy
--- a/Quot/Nominal/Perm.thy	Tue Feb 16 15:12:49 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Wed Feb 17 09:26:10 2010 +0100
@@ -46,32 +46,32 @@
   val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
 *}
 ML {*
-  fun perm_eq (i, (_, _, constrs)) =
-    map (fn (cname, dts) =>
-      let
-        val Ts = map (typ_of_dtyp descr sorts) dts;
-        val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
-        val args = map Free (names ~~ Ts);
-        val c = Const (cname, Ts ---> (nth_dtyp i));
-        fun perm_arg (dt, x) =
-          let val T = type_of x
-          in
-            if is_rec_type dt then
-              let val (Us, _) = strip_type T
-              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)
-                    ((length Us - 1 downto 0) ~~ Us)))
-              end
-            else (permute T) $ pi $ x
-          end;
-      in
-        (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (Free (nth perm_names_types' i) $
-             Free ("pi", @{typ perm}) $ list_comb (c, args),
-           list_comb (c, map perm_arg (dts ~~ args)))))
-      end) constrs;
+  fun perm_eq_constr i (cname, dts) =
+    let
+      val Ts = map (typ_of_dtyp descr sorts) dts;
+      val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
+      val args = map Free (names ~~ Ts);
+      val c = Const (cname, Ts ---> (nth_dtyp i));
+      fun perm_arg (dt, x) =
+        let val T = type_of x
+        in
+          if is_rec_type dt then
+            let val (Us, _) = strip_type T
+            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)
+                  ((length Us - 1 downto 0) ~~ Us)))
+            end
+          else (permute T) $ pi $ x
+        end;
+    in
+      (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
+        (Free (nth perm_names_types' i) $
+           Free ("pi", @{typ perm}) $ list_comb (c, args),
+         list_comb (c, map perm_arg (dts ~~ args)))))
+    end;
+  fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs;
   val perm_eqs = maps perm_eq descr;
 *}