# 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;