--- a/src/Tools/Code/code_ml.ML Sun May 29 14:10:48 2016 +0200
+++ b/src/Tools/Code/code_ml.ML Sun May 29 14:43:17 2016 +0200
@@ -772,13 +772,18 @@
fun modify_funs stmts = single (SOME
(Code_Namespace.Opaque, ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
fun modify_datatypes stmts =
- map_filter
- (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
- |> split_list
- |> apfst Code_Namespace.join_exports
- |> apsnd ML_Datas
- |> SOME
- |> single;
+ let
+ val datas = map_filter
+ (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
+ in
+ if null datas then [] (*for abstract types wrt. code_reflect*)
+ else datas
+ |> split_list
+ |> apfst Code_Namespace.join_exports
+ |> apsnd ML_Datas
+ |> SOME
+ |> single
+ end;
fun modify_class stmts =
the_single (map_filter
(fn (Type_Class class, (export, Code_Thingol.Class stmt)) => SOME (export, (class, stmt)) | _ => NONE) stmts)