src/Pure/Isar/code.ML

--- a/src/Pure/Isar/code.ML	Sat Jun 22 16:23:25 2019 +0200
+++ b/src/Pure/Isar/code.ML	Sun Jun 23 13:42:16 2019 +0000
@@ -336,6 +336,7 @@
         NONE => true
       | SOME (tyco, abs) => (case History.lookup types tyco of
           NONE => false
+        | SOME (_, Constructors _) => false
         | SOME (_, Abstractor {abstractor = (abs', _), projection, more_abstract_functions, ...}) =>
             abs = abs' andalso (c = projection orelse member (op =) more_abstract_functions c));
     fun check_datatypes (_, case_spec) =