src/Pure/proofterm.ML
changeset 33955 fff6f11b1f09
parent 33722 e588744f14da
child 33957 e9afca2118d4
     1.1 --- a/src/Pure/proofterm.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -1003,7 +1003,7 @@
     1.4                | _ => error "shrink: proof not in normal form");
     1.5              val vs = vars_of prop;
     1.6              val (ts', ts'') = chop (length vs) ts;
     1.7 -            val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
     1.8 +            val insts = (uncurry take) (length ts', map (fst o dest_Var) vs) ~~ ts';
     1.9              val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
    1.10                insert (op =) ixn (case AList.lookup (op =) insts ixn of
    1.11                    SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns'