src/Pure/type.ML

--- a/src/Pure/type.ML	Thu Mar 13 15:05:56 2014 +0100
+++ b/src/Pure/type.ML	Thu Mar 13 17:26:22 2014 +0100
@@ -26,6 +26,7 @@
     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
@@ -180,6 +181,9 @@
 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 =