# HG changeset patch
# User berghofe
# Date 1101288444 -3600
# Node ID 694f9d3ce90d8b4ddd7a4b625036e55c226c9593
# Parent  dfc2654eea9f0e537bef648a194f62a0ac65d4d4
Reimplemented some operations on "code lemma" table to avoid that code
lemmas get lost during merge.

diff -r dfc2654eea9f -r 694f9d3ce90d src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Wed Nov 24 10:23:36 2004 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Wed Nov 24 10:27:24 2004 +0100
@@ -23,7 +23,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val prep_ext = I;
-  val merge = Symtab.merge_multi Drule.eq_thm_prop;
+  val merge = Symtab.merge_multi' Drule.eq_thm_prop;
   fun print _ _ = ();
 end;
 
@@ -31,6 +31,7 @@
 
 val prop_of = #prop o rep_thm;
 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
+val lhs_of = fst o dest_eqn o prop_of;
 val const_of = dest_Const o head_of o fst o dest_eqn;
 
 fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
@@ -38,32 +39,39 @@
 
 fun add (p as (thy, thm)) =
   let
-    val tsig = Sign.tsig_of (sign_of thy);
     val tab = CodegenData.get thy;
     val (s, _) = const_of (prop_of thm);
-
-    val matches = curry
-      (Pattern.matches tsig o pairself (fst o dest_eqn o prop_of));
-
-  in (CodegenData.put (Symtab.update ((s,
-    filter_out (matches thm) (if_none (Symtab.lookup (tab, s)) []) @ [thm]),
-      tab)) thy, thm)
-  end handle TERM _ => (warn thm; p) | Pattern.Pattern => (warn thm; p);
+  in
+    if Pattern.pattern (lhs_of thm) then
+      (CodegenData.put (Symtab.update ((s,
+        thm :: if_none (Symtab.lookup (tab, s)) []), tab)) thy, thm)
+    else (warn thm; p)
+  end handle TERM _ => (warn thm; p);
 
 fun del (p as (thy, thm)) =
   let
     val tab = CodegenData.get thy;
     val (s, _) = const_of (prop_of thm);
-  in (CodegenData.put (Symtab.update ((s,
-    gen_rem eq_thm (if_none (Symtab.lookup (tab, s)) [], thm)),
-      tab)) thy, thm)
+  in case Symtab.lookup (tab, s) of
+      None => p
+    | Some thms => (CodegenData.put (Symtab.update ((s,
+        gen_rem eq_thm (thms, thm)), tab)) thy, thm)
   end handle TERM _ => (warn thm; p);
 
+fun del_redundant thy eqs [] = eqs
+  | del_redundant thy eqs (eq :: eqs') =
+    let
+      val tsig = Sign.tsig_of (sign_of thy);
+      val matches = curry
+        (Pattern.matches tsig o pairself lhs_of)
+    in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
+
 fun get_equations thy (s, T) =
   (case Symtab.lookup (CodegenData.get thy, s) of
      None => []
-   | Some thms => preprocess thy (filter (fn thm => is_instance thy T
-       (snd (const_of (prop_of thm)))) thms));
+   | Some thms => preprocess thy (del_redundant thy []
+       (filter (fn thm => is_instance thy T
+         (snd (const_of (prop_of thm)))) thms)));
 
 fun mk_poly_id thy (s, T) = mk_const_id (sign_of thy) s ^
   (case get_defn thy s T of