--- a/Quot/Nominal/Perm.thy	Tue Feb 16 14:57:39 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Tue Feb 16 15:12:49 2010 +0100
@@ -46,14 +46,13 @@
   val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
 *}
 ML {*
-  val perm_eqs = maps (fn (i, (_, _, constrs)) =>
-    let val T = nth_dtyp i
-    in map (fn (cname, dts) =>
+  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 ---> T);
+        val c = Const (cname, Ts ---> (nth_dtyp i));
         fun perm_arg (dt, x) =
           let val T = type_of x
           in
@@ -72,8 +71,8 @@
           (Free (nth perm_names_types' i) $
              Free ("pi", @{typ perm}) $ list_comb (c, args),
            list_comb (c, map perm_arg (dts ~~ args)))))
-      end) constrs
-    end) descr;
+      end) constrs;
+  val perm_eqs = maps perm_eq descr;
 *}
 
 local_setup {*
@@ -99,7 +98,7 @@
            ALLGOALS (asm_full_simp_tac @{simpset})];
      in
        map Drule.export_without_context (List.take (split_conj_thm
-         (Goal.prove_global @{theory} [] [] gl tac),
+         (Goal.prove @{context} [] [] gl tac),
        length new_type_names))
      end
 *}
@@ -110,7 +109,7 @@
    val pi2 = Free ("pi2", @{typ perm});
    val perm_append_thms =
       List.take (map Drule.export_without_context (split_conj_thm
-        (Goal.prove_global @{theory} [] []
+        (Goal.prove @{context} [] []
            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
               (map (fn ((s, T), x) =>
                   let