tuned;

--- a/src/Pure/pure_thy.ML	Thu Jul 25 18:29:04 2002 +0200
+++ b/src/Pure/pure_thy.ML	Fri Jul 26 21:07:57 2002 +0200
@@ -195,10 +195,10 @@
 
 (* hiding -- affects current theory node only! *)
 
-fun hide_thms b names thy =
+fun hide_thms fully names thy =
   let
     val r as ref {space, thms_tab, index} = get_theorems thy;
-    val space' = NameSpace.hide b (space, names);
+    val space' = NameSpace.hide fully (space, names);
   in r := {space = space', thms_tab = thms_tab, index = index}; thy end;