src/Pure/Isar/code.ML
changeset 24585 c359896d0f48
parent 24423 ae9cd0e92423
child 24624 b8383b1bbae3
     1.1 --- a/src/Pure/Isar/code.ML	Sat Sep 15 19:27:35 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Sat Sep 15 19:27:40 2007 +0200
     1.3 @@ -679,9 +679,9 @@
     1.4            then error ("Rejected equation for datatype constructor:\n"
     1.5              ^ string_of_thm func)
     1.6            else ();
     1.7 -      in map_exec_purge (SOME [c]) (map_funcs
     1.8 -        (Symtab.map_default
     1.9 -          (c, (Susp.value [], [])) (add_thm func))) thy
    1.10 +      in
    1.11 +        (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
    1.12 +          (c, (Susp.value [], [])) (add_thm func)) thy
    1.13        end
    1.14    | add_func false thm thy =
    1.15        case mk_func_liberal thm