src/Pure/Isar/code.ML
changeset 24659 6b7ac2a43df8
parent 24624 b8383b1bbae3
child 24731 c25aa6ae64ec
     1.1 --- a/src/Pure/Isar/code.ML	Thu Sep 20 16:37:30 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Sep 20 16:37:31 2007 +0200
     1.3 @@ -718,13 +718,13 @@
     1.4      | NONE => thy;
     1.5  
     1.6  fun del_func thm thy =
     1.7 -  let
     1.8 -    val func = mk_func thm;
     1.9 -    val const = const_of_func thy func;
    1.10 -  in map_exec_purge (SOME [const]) (map_funcs
    1.11 -    (Symtab.map_entry
    1.12 -      const (del_thm func))) thy
    1.13 -  end;
    1.14 +  case mk_liberal_func thm
    1.15 +   of SOME func => let
    1.16 +          val c = const_of_func thy func;
    1.17 +        in map_exec_purge (SOME [c]) (map_funcs
    1.18 +          (Symtab.map_entry c (del_thm func))) thy
    1.19 +        end
    1.20 +    | NONE => thy;
    1.21  
    1.22  fun add_funcl (const, lthms) thy =
    1.23    let