# HG changeset patch
# User wenzelm
# Date 1027710477 -7200
# Node ID 584a4a4c30ed52a25fb2b4f3a319e78fcd064eb9
# Parent  7ec771711c09f22939aece1de15fb66a3378020b
tuned;

diff -r 7ec771711c09 -r 584a4a4c30ed src/Pure/pure_thy.ML
--- 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;