Added "del" attribute for deleting equations.
authorberghofe
Mon Sep 22 16:14:58 2003 +0200 (2003-09-22)
changeset 14196be5e838f37bd
parent 14195 e7c9206dd2ef
child 14197 3d7c6fc7c66e
Added "del" attribute for deleting equations.
src/HOL/Tools/recfun_codegen.ML
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Mon Sep 22 16:06:05 2003 +0200
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Mon Sep 22 16:14:58 2003 +0200
     1.3 @@ -51,6 +51,15 @@
     1.4        tab)) thy, thm)
     1.5    end handle TERM _ => (warn thm; p) | Pattern.Pattern => (warn thm; p);
     1.6  
     1.7 +fun del (p as (thy, thm)) =
     1.8 +  let
     1.9 +    val tab = CodegenData.get thy;
    1.10 +    val (s, _) = const_of (prop_of thm);
    1.11 +  in (CodegenData.put (Symtab.update ((s,
    1.12 +    gen_rem eq_thm (if_none (Symtab.lookup (tab, s)) [], thm)),
    1.13 +      tab)) thy, thm)
    1.14 +  end handle TERM _ => (warn thm; p);
    1.15 +
    1.16  fun get_equations thy (s, T) =
    1.17    (case Symtab.lookup (CodegenData.get thy, s) of
    1.18       None => []
    1.19 @@ -139,6 +148,6 @@
    1.20  val setup =
    1.21    [CodegenData.init,
    1.22     add_codegen "recfun" recfun_codegen,
    1.23 -   add_attribute "" add];
    1.24 +   add_attribute "" (Args.del |-- Scan.succeed del || Scan.succeed add)];
    1.25  
    1.26  end;