author | wenzelm |
Sat, 11 Jun 2005 22:15:56 +0200 | |
changeset 16371 | d30742f22121 |
parent 16370 | 033d890fe91f |
child 16372 | 8618d334840b |
--- 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 *)