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;