src/HOL/Library/reflection.ML
changeset 30148 5d04b67a866e
parent 29834 3237cfd177f3
child 30743 2c83f7eaf1a4
     1.1 --- a/src/HOL/Library/reflection.ML	Fri Feb 27 16:54:49 2009 +0100
     1.2 +++ b/src/HOL/Library/reflection.ML	Fri Feb 27 18:03:47 2009 +0100
     1.3 @@ -88,17 +88,12 @@
     1.4  
     1.5  fun dest_listT (Type ("List.list", [T])) = T;
     1.6  
     1.7 -fun partition P [] = ([],[])
     1.8 -  | partition P (x::xs) = 
     1.9 -     let val (yes,no) = partition P xs
    1.10 -     in if P x then (x::yes,no) else (yes, x::no) end
    1.11 -
    1.12  fun rearrange congs = 
    1.13  let 
    1.14   fun P (_, th) = 
    1.15    let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th
    1.16    in can dest_Var l end
    1.17 - val (yes,no) = partition P congs 
    1.18 + val (yes,no) = List.partition P congs 
    1.19   in no @ yes end
    1.20  
    1.21  fun genreif ctxt raw_eqs t =