# HG changeset patch
# User wenzelm
# Date 1575648352 -3600
# Node ID a624319011409e2fbf31532508dde07ef0438a34
# Parent  c5914bdd896bae401988a565db385a20a162f923
suppress record types: not working properly;

diff -r c5914bdd896b -r a62431901140 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 06 16:22:15 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 06 17:05:52 2019 +0100
@@ -1246,7 +1246,7 @@
     val datatypes =
       (Data.get (Context.Theory thy), []) |-> Symtab.fold
         (fn (name, (pos, {kind, T, ctrs, ...})) =>
-          if exists (fn tab => Symtab.defined tab name) parents then I
+          if kind = Record orelse exists (fn tab => Symtab.defined tab name) parents then I
           else
             let
               val pos_properties = Thy_Info.adjust_pos_properties context pos;