renamed IsarThy.hide_space to IsarThy.hide_names;
authorwenzelm
Sat, 11 Jun 2005 22:15:56 +0200
changeset 16371 d30742f22121
parent 16370 033d890fe91f
child 16372 8618d334840b
renamed IsarThy.hide_space to IsarThy.hide_names;
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 *)