1.1 --- a/src/Pure/Isar/code.ML Thu Jan 31 11:44:43 2008 +0100
1.2 +++ b/src/Pure/Isar/code.ML Thu Jan 31 11:44:46 2008 +0100
1.3 @@ -13,6 +13,7 @@
1.4 val add_default_func: thm -> theory -> theory
1.5 val add_default_func_attr: Attrib.src
1.6 val del_func: thm -> theory -> theory
1.7 + val del_funcs: string -> theory -> theory
1.8 val add_funcl: string * thm list Susp.T -> theory -> theory
1.9 val add_inline: thm -> theory -> theory
1.10 val del_inline: thm -> theory -> theory
1.11 @@ -162,6 +163,11 @@
1.12 fun del_thm thm (sels, dels) =
1.13 (Susp.value (remove Thm.eq_thm_prop thm (Susp.force sels)), thm :: dels);
1.14
1.15 +fun del_thms (sels, dels) =
1.16 + let
1.17 + val all_sels = Susp.force sels;
1.18 + in (Susp.value [], rev all_sels @ dels) end;
1.19 +
1.20 fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
1.21
1.22
1.23 @@ -770,6 +776,9 @@
1.24 end
1.25 | NONE => thy;
1.26
1.27 +fun del_funcs const = map_exec_purge (SOME [const])
1.28 + (map_funcs (Symtab.map_entry const (apsnd del_thms)));
1.29 +
1.30 fun add_funcl (const, lthms) thy =
1.31 let
1.32 val lthms' = certificate thy (fn thy => certify_const thy const) lthms;