src/Pure/Isar/isar_syn.ML
changeset 26672 f99956db6ccd
parent 26619 c348bbe7c87d
child 26676 fb8039e26c6a
--- 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 *)