src/HOL/Tools/recfun_codegen.ML

 
   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);
+
+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 => []
    | Some thms => filter (fn thm => is_instance thy T

 
 
 val setup =
   [CodegenData.init,
    add_codegen "recfun" recfun_codegen,
-   add_attribute "" add];
+   add_attribute "" (Args.del |-- Scan.succeed del || Scan.succeed add)];
 
 end;