# HG changeset patch
# User haftmann
# Date 1514839325 0
# Node ID 89be5a4f514b5829758b7e243f6027b63b238065
# Parent  17fdb2c98083b36f76398669be5f5f97056e9c47
skip abstract constructors silently in datatype clauses of computations

diff -r 17fdb2c98083 -r 89be5a4f514b src/Doc/Codegen/Computations.thy
--- 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
diff -r 17fdb2c98083 -r 89be5a4f514b src/Tools/Code/code_runtime.ML
--- 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