--- a/src/HOL/Tools/TFL/thry.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/TFL/thry.ML Thu Oct 15 23:28:10 2009 +0200
@@ -73,9 +73,9 @@
constructors = (map Const o the o Datatype.get_constrs thy) dtco};
fun extract_info thy =
- let val infos = (map snd o Symtab.dest o Datatype.get_all) thy
+ let val infos = map snd (Symtab.dest (Datatype.get_all thy))
in {case_congs = map (mk_meta_eq o #case_cong) infos,
- case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
+ case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
end;