suppress record types: not working properly;
authorwenzelm
Fri, 06 Dec 2019 17:05:52 +0100
changeset 71253 a62431901140
parent 71252 c5914bdd896b
child 71254 a9ad4a954cb7
suppress record types: not working properly;
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;