Adapted to changed type of add_typedef_i.

--- a/src/HOL/Nominal/nominal_package.ML	Mon Apr 10 11:35:02 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Mon Apr 10 14:37:23 2006 +0200
@@ -552,7 +552,7 @@
           (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
             (rtac exI 1 THEN
               QUIET_BREADTH_FIRST (has_fewer_prems 1)
-              (resolve_tac rep_intrs 1))) thy |> (fn (thy, r) =>
+              (resolve_tac rep_intrs 1))) thy |> (fn (r, thy) =>
         let
           val permT = mk_permT (TFree (variant tvs "'a", HOLogic.typeS));
           val pi = Free ("pi", permT);