TFL/thry.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15798 016f3be5a5ec
--- 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;