# HG changeset patch
# User berghofe
# Date 1144672643 -7200
# Node ID 5c15cd397a82e71288a74ec5ac19f3ae2fc90cb5
# Parent  742b7934ccfcbe344e2ef00ef10b371fd49e5dfe
Adapted to changed type of add_typedef_i.

diff -r 742b7934ccfc -r 5c15cd397a82 src/HOL/Nominal/nominal_package.ML
--- 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);