src/Pure/Isar/obtain.ML
changeset 33955 fff6f11b1f09
parent 33389 bb3a5fa94a91
child 33957 e9afca2118d4
     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -232,12 +232,12 @@
     1.4          err ("Failed to unify variable " ^
     1.5            string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^
     1.6            string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
     1.7 -    val (tyenv, _) = fold unify (map #1 vars ~~ Library.take (m, params))
     1.8 +    val (tyenv, _) = fold unify (map #1 vars ~~ (uncurry take) (m, params))
     1.9        (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
    1.10      val norm_type = Envir.norm_type tyenv;
    1.11  
    1.12      val xs = map (apsnd norm_type o fst) vars;
    1.13 -    val ys = map (apsnd norm_type) (Library.drop (m, params));
    1.14 +    val ys = map (apsnd norm_type) ((uncurry drop) (m, params));
    1.15      val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
    1.16      val terms = map (Drule.mk_term o cert o Free) (xs @ ys');
    1.17