# HG changeset patch
# User wenzelm
# Date 1118520956 -7200
# Node ID d30742f22121ad778afc744fdaf4e898ccb89628
# Parent  033d890fe91f961d238ec1587b93d0ac63e2673e
renamed IsarThy.hide_space to IsarThy.hide_names;

diff -r 033d890fe91f -r d30742f22121 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Jun 11 22:15:55 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jun 11 22:15:56 2005 +0200
@@ -229,7 +229,7 @@
 
 val hideP =
   OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
-    (P.name -- Scan.repeat1 P.xname >> (Toplevel.theory o IsarThy.hide_space));
+    (P.name -- Scan.repeat1 P.xname >> (Toplevel.theory o IsarThy.hide_names));
 
 
 (* use ML text *)