src/Pure/Isar/code.ML

   val add_func: thm -> theory -> theory
   val add_liberal_func: thm -> theory -> theory
   val add_default_func: thm -> theory -> theory
   val add_default_func_attr: Attrib.src
   val del_func: thm -> theory -> theory
+  val del_funcs: string -> theory -> theory
   val add_funcl: string * thm list Susp.T -> theory -> theory
   val add_inline: thm -> theory -> theory
   val del_inline: thm -> theory -> theory
   val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory
   val del_inline_proc: string -> theory -> theory

   | add_lthms lthms (sels, dels) =
       fold add_thm (Susp.force lthms) (sels, dels);
 
 fun del_thm thm (sels, dels) =
   (Susp.value (remove Thm.eq_thm_prop thm (Susp.force sels)), thm :: dels);
+
+fun del_thms (sels, dels) =
+  let
+    val all_sels = Susp.force sels;
+  in (Susp.value [], rev all_sels @ dels) end;
 
 fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
 
 
 (* fundamental melting operations *)

         in map_exec_purge (SOME [c]) (map_funcs
           (Symtab.map_entry c (apsnd (del_thm func)))) thy
         end
     | NONE => thy;
 
+fun del_funcs const = map_exec_purge (SOME [const])
+  (map_funcs (Symtab.map_entry const (apsnd del_thms)));
+
 fun add_funcl (const, lthms) thy =
   let
     val lthms' = certificate thy (fn thy => certify_const thy const) lthms;
       (*FIXME must check compatibility with sort algebra;
         alas, naive checking results in non-termination!*)