changeset 61260 | e6f03fae14d5 |
parent 61110 | 6b7c2ecc6aea |
child 61466 | 9a468c3a1fa1 |
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Wed Sep 23 09:50:38 2015 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Sep 24 13:33:42 2015 +0200 @@ -186,7 +186,7 @@ |> Sign.parent_path |> fold_map (fn (((name, mx), tvs), c) => - Typedef.add_typedef_global (name, tvs, mx) + Typedef.add_typedef_global {overloaded = false} (name, tvs, mx) (Collect $ Const (c, UnivT')) NONE (fn ctxt => resolve_tac ctxt [exI] 1 THEN