# HG changeset patch
# User berghofe
# Date 1008858222 -3600
# Node ID 323ce5a8969519bf04fc37d0de2e344f95c62463
# Parent  8cf9d9a3a327da25e43f45c59776658f4bc47586
Fixed bug in function add.

diff -r 8cf9d9a3a327 -r 323ce5a89695 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Dec 20 15:20:07 2001 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Dec 20 15:23:42 2001 +0100
@@ -36,19 +36,14 @@
   string_of_thm thm);
 
 fun add (p as (thy, thm)) =
-  let
-    val tsig = Sign.tsig_of (sign_of thy);
-    val tab = CodegenData.get thy;
-    val matches = curry (Pattern.matches tsig o pairself concl_of);
-
+  let val tab = CodegenData.get thy;
   in (case concl_of thm of
       _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
         Const (s, _) => (CodegenData.put (Symtab.update ((s,
-          filter_out (matches thm) (if_none (Symtab.lookup (tab, s)) []) @
-            [thm]), tab)) thy, thm)
+          if_none (Symtab.lookup (tab, s)) [] @ [thm]), tab)) thy, thm)
       | _ => (warn thm; p))
     | _ => (warn thm; p))
-  end handle Pattern.Pattern => (warn thm; p);
+  end;
 
 fun get_clauses thy s =
   (case Symtab.lookup (CodegenData.get thy, s) of