# HG changeset patch
# User haftmann
# Date 1167937261 -3600
# Node ID 9dc365b035730842c476f1fbd72c6e0c18bc9ecf
# Parent  0faa5afd5d69e880c7dea856a9f3d78f0d05a147
dropped function theorems are considered as deleted

diff -r 0faa5afd5d69 -r 9dc365b03573 src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Thu Jan 04 20:01:00 2007 +0100
+++ b/src/Pure/Tools/codegen_data.ML	Thu Jan 04 20:01:01 2007 +0100
@@ -248,26 +248,27 @@
 
 type sdthms = thm list Susp.T * thm list;
 
-fun add_drop_redundant thm thms =
+fun add_drop_redundant thm (sels, dels) =
   let
-    val thy = Context.check_thy (Thm.theory_of_thm thm);
+    val thy = Thm.theory_of_thm thm;
     val args_of = snd o strip_comb o fst o Logic.dest_equals o Drule.plain_prop_of;
     val args = args_of thm;
     fun matches [] _ = true
       | matches (Var _ :: xs) [] = matches xs []
       | matches (_ :: _) [] = false
       | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys;
-    fun drop thm' = if matches args (args_of thm')
-      then (warning ("Dropping redundant function theorem\n" ^ string_of_thm thm'); false)
-      else true
-  in thm :: filter drop thms end;
+    fun drop thm' = not (matches args (args_of thm'))
+      orelse (warning ("Dropping redundant function theorem\n" ^ string_of_thm thm'); false);
+    val (keeps, drops) = List.partition drop sels;
+  in (thm :: keeps, dels |> fold (insert eq_thm) drops |> remove eq_thm thm) end;
 
 fun add_thm thm (sels, dels) =
-  (Susp.value (add_drop_redundant thm (Susp.force sels)), remove eq_thm thm dels);
+  apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels));
 
 fun add_lthms lthms (sels, []) =
       (lazy (fn () => fold add_drop_redundant
-          (Susp.force lthms) (Susp.force sels)), [])
+        (Susp.force lthms) (Susp.force sels, []) |> fst), [])
+        (*FIXME*)
   | add_lthms lthms (sels, dels) =
       fold add_thm (Susp.force lthms) (sels, dels);