--- a/src/Doc/Codegen/Computations.thy Tue Jan 02 21:32:14 2018 +0100
+++ b/src/Doc/Codegen/Computations.thy Mon Jan 01 20:42:05 2018 +0000
@@ -131,7 +131,8 @@
\<^item> Each type following @{text "datatypes:"} specifies all constructors
of the corresponding code datatype as input constants. Note that
this does not increase expressiveness but succinctness for datatypes
- with many constructors.
+ with many constructors. Abstract type constructors are skipped
+ silently.
\<^item> The code generated by a @{text computation} antiquotation takes a functional argument
which describes how to conclude the computation. What's the rationale
--- a/src/Tools/Code/code_runtime.ML Tue Jan 02 21:32:14 2018 +0100
+++ b/src/Tools/Code/code_runtime.ML Mon Jan 01 20:42:05 2018 +0000
@@ -598,16 +598,18 @@
fun add_all_constrs ctxt (dT as Type (tyco, Ts)) =
- let
- val ((vs, constrs), _) = Code.get_type (Proof_Context.theory_of ctxt) tyco;
- val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts);
- val cs = map (fn (c, (_, Ts')) =>
- (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts'
- ---> dT)) constrs;
- in
- union (op =) cs
- #> fold (add_all_constrs ctxt) Ts
- end;
+ case Code.get_type (Proof_Context.theory_of ctxt) tyco of
+ ((vs, constrs), false) =>
+ let
+ val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts);
+ val cs = map (fn (c, (_, Ts')) =>
+ (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts'
+ ---> dT)) constrs;
+ in
+ union (op =) cs
+ #> fold (add_all_constrs ctxt) Ts
+ end
+ | (_, true) => I;
fun prep_spec ctxt (raw_ts, raw_dTs) =
let