--- a/src/Pure/Isar/code.ML Sat Sep 15 19:27:35 2007 +0200
+++ b/src/Pure/Isar/code.ML Sat Sep 15 19:27:40 2007 +0200
@@ -679,9 +679,9 @@
then error ("Rejected equation for datatype constructor:\n"
^ string_of_thm func)
else ();
- in map_exec_purge (SOME [c]) (map_funcs
- (Symtab.map_default
- (c, (Susp.value [], [])) (add_thm func))) thy
+ in
+ (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
+ (c, (Susp.value [], [])) (add_thm func)) thy
end
| add_func false thm thy =
case mk_func_liberal thm