proper quasi-total merge
authorhaftmann
Sun Jun 23 13:42:16 2019 +0000 (4 weeks ago)
changeset 70358a55cfc8566fd
parent 70357 4d0b789e4e21
child 70359 470d4f145e4c
proper quasi-total merge
src/Pure/Isar/code.ML
     1.1 --- a/src/Pure/Isar/code.ML	Sat Jun 22 16:23:25 2019 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Sun Jun 23 13:42:16 2019 +0000
     1.3 @@ -336,6 +336,7 @@
     1.4          NONE => true
     1.5        | SOME (tyco, abs) => (case History.lookup types tyco of
     1.6            NONE => false
     1.7 +        | SOME (_, Constructors _) => false
     1.8          | SOME (_, Abstractor {abstractor = (abs', _), projection, more_abstract_functions, ...}) =>
     1.9              abs = abs' andalso (c = projection orelse member (op =) more_abstract_functions c));
    1.10      fun check_datatypes (_, case_spec) =