src/Pure/assumption.ML
changeset 33955 fff6f11b1f09
parent 33519 e31a85f92ce9
child 33957 e9afca2118d4
     1.1 --- a/src/Pure/assumption.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/Pure/assumption.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -88,12 +88,12 @@
     1.4  (* local assumptions *)
     1.5  
     1.6  fun local_assumptions_of inner outer =
     1.7 -  Library.drop (length (all_assumptions_of outer), all_assumptions_of inner);
     1.8 +  (uncurry drop) (length (all_assumptions_of outer), all_assumptions_of inner);
     1.9  
    1.10  val local_assms_of = maps #2 oo local_assumptions_of;
    1.11  
    1.12  fun local_prems_of inner outer =
    1.13 -  Library.drop (length (all_prems_of outer), all_prems_of inner);
    1.14 +  (uncurry drop) (length (all_prems_of outer), all_prems_of inner);
    1.15  
    1.16  
    1.17  (* add assumptions *)