src/HOL/Nominal/nominal_package.ML
changeset 19403 5c15cd397a82
parent 19322 bf84bdf05f14
child 19489 4441b637871b
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Mon Apr 10 11:35:02 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Apr 10 14:37:23 2006 +0200
     1.3 @@ -552,7 +552,7 @@
     1.4            (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
     1.5              (rtac exI 1 THEN
     1.6                QUIET_BREADTH_FIRST (has_fewer_prems 1)
     1.7 -              (resolve_tac rep_intrs 1))) thy |> (fn (thy, r) =>
     1.8 +              (resolve_tac rep_intrs 1))) thy |> (fn (r, thy) =>
     1.9          let
    1.10            val permT = mk_permT (TFree (variant tvs "'a", HOLogic.typeS));
    1.11            val pi = Free ("pi", permT);