diff -r c95590e01df5 -r f99956db6ccd src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Apr 15 18:49:26 2008 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Apr 15 18:49:27 2008 +0200 @@ -296,7 +296,7 @@ val _ = OuterSyntax.command "hide" "hide names from given name space" K.thy_decl ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >> - (Toplevel.theory o uncurry Sign.hide_names)); + (Toplevel.theory o uncurry IsarCmd.hide_names)); (* use ML text *)