# HG changeset patch
# User berghofe
# Date 1064240098 -7200
# Node ID be5e838f37bd2e7af7d136d4886d7ce3708c2a15
# Parent  e7c9206dd2ef7ef88088061da509032694de64c9
Added "del" attribute for deleting equations.

diff -r e7c9206dd2ef -r be5e838f37bd src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Mon Sep 22 16:06:05 2003 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Mon Sep 22 16:14:58 2003 +0200
@@ -51,6 +51,15 @@
       tab)) thy, thm)
   end handle TERM _ => (warn thm; p) | Pattern.Pattern => (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)
+  end handle TERM _ => (warn thm; p);
+
 fun get_equations thy (s, T) =
   (case Symtab.lookup (CodegenData.get thy, s) of
      None => []
@@ -139,6 +148,6 @@
 val setup =
   [CodegenData.init,
    add_codegen "recfun" recfun_codegen,
-   add_attribute "" add];
+   add_attribute "" (Args.del |-- Scan.succeed del || Scan.succeed add)];
 
 end;