--- a/TFL/thry.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/TFL/thry.ML Thu Mar 03 12:43:01 2005 +0100
@@ -66,12 +66,12 @@
NONE => NONE
| SOME {nchotomy, ...} =>
SOME {nchotomy = nchotomy,
- constructors = the (DatatypePackage.constrs_of thy tname)};
+ constructors = valOf (DatatypePackage.constrs_of thy tname)};
fun extract_info thy =
let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
in {case_congs = map (mk_meta_eq o #case_cong) infos,
- case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)}
+ case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
end;