# 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