1.1 --- a/src/Pure/Tools/codegen_data.ML	Thu Jan 04 20:01:00 2007 +0100
     1.2 +++ b/src/Pure/Tools/codegen_data.ML	Thu Jan 04 20:01:01 2007 +0100
     1.3 @@ -248,26 +248,27 @@
     1.4  
     1.5  type sdthms = thm list Susp.T * thm list;
     1.6  
     1.7 -fun add_drop_redundant thm thms =
     1.8 +fun add_drop_redundant thm (sels, dels) =
     1.9    let
    1.10 -    val thy = Context.check_thy (Thm.theory_of_thm thm);
    1.11 +    val thy = Thm.theory_of_thm thm;
    1.12      val args_of = snd o strip_comb o fst o Logic.dest_equals o Drule.plain_prop_of;
    1.13      val args = args_of thm;
    1.14      fun matches [] _ = true
    1.15        | matches (Var _ :: xs) [] = matches xs []
    1.16        | matches (_ :: _) [] = false
    1.17        | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys;
    1.18 -    fun drop thm' = if matches args (args_of thm')
    1.19 -      then (warning ("Dropping redundant function theorem\n" ^ string_of_thm thm'); false)
    1.20 -      else true
    1.21 -  in thm :: filter drop thms end;
    1.22 +    fun drop thm' = not (matches args (args_of thm'))
    1.23 +      orelse (warning ("Dropping redundant function theorem\n" ^ string_of_thm thm'); false);
    1.24 +    val (keeps, drops) = List.partition drop sels;
    1.25 +  in (thm :: keeps, dels |> fold (insert eq_thm) drops |> remove eq_thm thm) end;
    1.26  
    1.27  fun add_thm thm (sels, dels) =
    1.28 -  (Susp.value (add_drop_redundant thm (Susp.force sels)), remove eq_thm thm dels);
    1.29 +  apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels));
    1.30  
    1.31  fun add_lthms lthms (sels, []) =
    1.32        (lazy (fn () => fold add_drop_redundant
    1.33 -          (Susp.force lthms) (Susp.force sels)), [])
    1.34 +        (Susp.force lthms) (Susp.force sels, []) |> fst), [])
    1.35 +        (*FIXME*)
    1.36    | add_lthms lthms (sels, dels) =
    1.37        fold add_thm (Susp.force lthms) (sels, dels);
    1.38