src/Pure/type.ML

    {classes: Name_Space.T * Sorts.algebra,
     default: sort,
     types: decl Name_Space.table,
     log_types: string list}
   val change_base: bool -> tsig -> tsig
+  val change_ignore: tsig -> tsig
   val empty_tsig: tsig
   val class_space: tsig -> Name_Space.T
   val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
   val defaultS: tsig -> sort
   val logical_types: tsig -> string list

   TSig {classes = classes, default = default, types = types, log_types = log_types};
 
 fun change_base begin (TSig {classes, default, types, log_types}) =
   make_tsig (classes, default, Name_Space.change_base begin types, log_types);
 
+fun change_ignore (TSig {classes, default, types, log_types}) =
+  make_tsig (classes, default, Name_Space.change_ignore types, log_types);
+
 fun build_tsig (classes, default, types) =
   let
     val log_types =
       Name_Space.fold_table (fn (c, LogicalType n) => cons (c, n) | _ => I) types []
       |> Library.sort (int_ord o pairself snd) |> map fst;