src/HOL/Nominal/nominal_induct.ML
changeset 33957 e9afca2118d4
parent 33955 fff6f11b1f09
child 34907 b0aaec87751c
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Tue Nov 24 17:28:44 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Wed Nov 25 09:13:46 2009 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4          val m = length vars and n = length inst;
     1.5          val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule";
     1.6          val P :: x :: ys = vars;
     1.7 -        val zs = (uncurry drop) (m - n - 2, ys);
     1.8 +        val zs = drop (m - n - 2) ys;
     1.9        in
    1.10          (P, tuple_fun (map #2 avoiding) (Term.dest_Var P)) ::
    1.11          (x, tuple (map Free avoiding)) ::
    1.12 @@ -71,7 +71,7 @@
    1.13          val p = length ps;
    1.14          val ys =
    1.15            if p < n then []
    1.16 -          else map (tune o #1) ((uncurry take) (p - n, ps)) @ xs;
    1.17 +          else map (tune o #1) (take (p - n) ps) @ xs;
    1.18        in Logic.list_rename_params (ys, prem) end;
    1.19      fun rename_prems prop =
    1.20        let val (As, C) = Logic.strip_horn (Thm.prop_of rule)