changeset 19403 | 5c15cd397a82 |
parent 19322 | bf84bdf05f14 |
child 19489 | 4441b637871b |
--- 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);