src/HOL/Tools/Old_Datatype/old_datatype.ML

 
     val (typedefs, thy3) = thy2
       |> 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
               resolve_tac ctxt [CollectI] 1 THEN
               QUIET_BREADTH_FIRST (has_fewer_prems 1)