--- a/src/Pure/Isar/code.ML Thu Sep 20 16:37:30 2007 +0200
+++ b/src/Pure/Isar/code.ML Thu Sep 20 16:37:31 2007 +0200
@@ -718,13 +718,13 @@
| NONE => thy;
fun del_func thm thy =
- let
- val func = mk_func thm;
- val const = const_of_func thy func;
- in map_exec_purge (SOME [const]) (map_funcs
- (Symtab.map_entry
- const (del_thm func))) thy
- end;
+ case mk_liberal_func thm
+ of SOME func => let
+ val c = const_of_func thy func;
+ in map_exec_purge (SOME [c]) (map_funcs
+ (Symtab.map_entry c (del_thm func))) thy
+ end
+ | NONE => thy;
fun add_funcl (const, lthms) thy =
let