# HG changeset patch
# User wenzelm
# Date 1208278164 -7200
# Node ID c27efd6de25d9578a801d5dae7e3ab2f388642b3
# Parent  65023d4fd226a7b09a8d8648e932816360206440
simplified hide_XXX interfaces;

diff -r 65023d4fd226 -r c27efd6de25d src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Apr 15 18:49:23 2008 +0200
+++ b/src/Pure/type.ML	Tue Apr 15 18:49:24 2008 +0200
@@ -70,12 +70,12 @@
 
   (*extend and merge type signatures*)
   val add_class: Pretty.pp -> NameSpace.naming -> bstring * class list -> tsig -> tsig
-  val hide_classes: bool -> string list -> tsig -> tsig
+  val hide_class: bool -> string -> tsig -> tsig
   val set_defsort: sort -> tsig -> tsig
   val add_types: NameSpace.naming -> (bstring * int) list -> tsig -> tsig
   val add_abbrevs: NameSpace.naming -> (string * string list * typ) list -> tsig -> tsig
   val add_nonterminals: NameSpace.naming -> string list -> tsig -> tsig
-  val hide_types: bool -> string list -> tsig -> tsig
+  val hide_type: bool -> string -> tsig -> tsig
   val add_arity: Pretty.pp -> arity -> tsig -> tsig
   val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
   val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig
@@ -505,8 +505,8 @@
       val classes' = classes |> Sorts.add_class pp (c', cs');
     in ((space', classes'), default, types) end);
 
-fun hide_classes fully cs = map_tsig (fn ((space, classes), default, types) =>
-  ((fold (NameSpace.hide fully) cs space, classes), default, types));
+fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
+  ((NameSpace.hide fully c space, classes), default, types));
 
 
 (* arities *)
@@ -608,8 +608,8 @@
 
 end;
 
-fun hide_types fully cs = map_tsig (fn (classes, default, (space, types)) =>
-  (classes, default, (fold (NameSpace.hide fully) cs space, types)));
+fun hide_type fully c = map_tsig (fn (classes, default, (space, types)) =>
+  (classes, default, (NameSpace.hide fully c space, types)));
 
 
 (* merge type signatures *)